1  /-
  2  Copyright (c) 2018 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Mario Carneiro
  5  
  6  Ordinal notations (constructive ordinal arithmetic for ordinals < ε₀).
  7  -/
  8  import set_theory.ordinal data.pnat.basic
src         └────────────────┘ └─────────────┘
  9  open ordinal
 10  open_locale ordinal -- get notation for `ω`
 11  
 12  /-- Recursive definition of an ordinal notation. `zero` denotes the
 13    ordinal 0, and `oadd e n a` is intended to refer to `ω^e * n + a`.
 14    For this to be valid Cantor normal form, we must have the exponents
 15    decrease to the right, but we can't state this condition until we've
 16    defined `repr`, so it is a separate definition `NF`. -/
 17  @[derive decidable_eq]
id            └──────────┘
src           └──────────┘
typ           └──────────┘
doc    └────┘
 18  inductive onote : Type
 19  | zero : onote
 20  | oadd : onote → ℕ+ → onote → onote
id                    └┘
src                   └┘
typ                   └┘
doc                   └┘
 21  
 22  namespace onote
 23  
 24  /-- Notation for 0 -/
 25  instance : has_zero onote := ⟨zero⟩
id              └──────┘ └───┘     └──┘
src             └──────┘ └───┘     └──┘
typ             └──────┘ └───┘     └──┘
doc                      └───┘
 26  @[simp] theorem zero_def : zero = 0 := rfl
id                              └──┘       └─┘
src                             └──┘       └─┘
typ                             └──┘       └─┘
doc    └──┘
 27  
 28  instance : inhabited onote := ⟨0⟩
id              └───────┘ └───┘
src             └───────┘ └───┘
typ             └───────┘ └───┘
doc                       └───┘
 29  
 30  /-- Notation for 1 -/
 31  instance : has_one onote := ⟨oadd 0 1 0⟩
id              └─────┘ └───┘     └──┘
src             └─────┘ └───┘     └──┘
typ             └─────┘ └───┘     └──┘
doc                     └───┘
 32  
 33  /-- Notation for ω -/
 34  def omega : onote := oadd 1 1 0
id               └───┘    └──┘
src              └───┘    └──┘
typ              └───┘    └──┘
doc              └───┘
 35  
 36  /-- The ordinal denoted by a notation -/
 37  @[simp] noncomputable def repr : onote → ordinal.{0}
id                                    └───┘  └─────┘
src                                   └───┘  └─────┘
typ                                   └───┘  └─────┘
doc    └──┘                           └───┘   └─────┘
 38  | 0 := 0
 39  | (oadd e n a) := ω ^ repr e * n + repr a
id      └──┘          └──┘       └──┘
src     └──┘             └──┘       └──┘
typ     └──┘          └──┘       └──┘
doc                    
 40  
 41  def to_string_aux1 (e : onote) (n : ℕ) (s : string) : string :=
id                           └───┘              └────┘    └────┘
src                          └───┘              └────┘    └────┘
typ                          └───┘              └────┘    └────┘
doc                          └───┘
 42  if e = 0 then _root_.to_string n else
id               └──────────────┘ 
src               └──────────────┘
typ              └──────────────┘ 
 43  (if e = 1 then "ω" else "ω^(" ++ s ++ ")") ++
id                               └┘  └┘      └┘
src                               └┘   └┘      └┘
typ                              └┘  └┘      └┘
 44  if n = 1 then "" else "*" ++ _root_.to_string n
id                           └┘ └──────────────┘ 
src                           └┘ └──────────────┘
typ                          └┘ └──────────────┘ 
 45  
 46  /-- Print an ordinal notation -/
 47  def to_string : onote → string
id                   └───┘  └────┘
src                  └───┘  └────┘
typ                  └───┘  └────┘
doc                  └───┘
 48  | zero := "0"
id     └──┘
src    └──┘
typ    └──┘
 49  | (oadd e n 0) := to_string_aux1 e n (to_string e)
id      └──┘         └────────────┘      └───────┘
src     └──┘           └────────────┘      └───────┘
typ     └──┘         └────────────┘      └───────┘
 50  | (oadd e n a) := to_string_aux1 e n (to_string e) ++ " + " ++ to_string a
id      └──┘        └────────────┘      └───────┘    └┘       └┘ └───────┘
src     └──┘           └────────────┘      └───────┘    └┘       └┘ └───────┘
typ     └──┘        └────────────┘      └───────┘    └┘       └┘ └───────┘
 51  
 52  /-- Print an ordinal notation -/
 53  def repr' : onote → string
id               └───┘  └────┘
src              └───┘   └────┘
typ              └───┘  └────┘
doc              └───┘
 54  | zero := "0"
id     └──┘
src    └──┘
typ    └──┘
 55  | (oadd e n a) := "(oadd " ++ repr' e ++ " " ++ _root_.to_string (n:ℕ) ++ " " ++ repr' a ++ ")"
id      └──┘                 └┘ └───┘   └┘     └┘ └──────────────┘      └┘     └┘ └───┘   └┘
src     └──┘                    └┘         └┘     └┘ └──────────────┘      └┘     └┘         └┘
typ     └──┘                 └┘ └───┘   └┘     └┘ └──────────────┘      └┘     └┘ └───┘   └┘
 56  
 57  instance : has_to_string onote := ⟨to_string⟩
id              └───────────┘ └───┘     └───────┘
src             └───────────┘ └───┘     └───────┘
typ             └───────────┘ └───┘     └───────┘
doc                           └───┘     └───────┘
 58  instance : has_repr onote := ⟨repr'⟩
id              └──────┘ └───┘     └───┘
src             └──────┘ └───┘     └───┘
typ             └──────┘ └───┘     └───┘
doc                      └───┘     └───┘
 59  
 60  instance : preorder onote :=
id              └──────┘ └───┘
src             └──────┘ └───┘
typ             └──────┘ └───┘
doc                      └───┘
 61  { le       := λ x y, repr x ≤ repr y,
id                      └──┘   └──┘ 
src                       └──┘    └──┘
typ                     └──┘   └──┘ 
doc                       └──┘     └──┘
 62    lt       := λ x y, repr x < repr y,
id                      └──┘   └──┘ 
src                       └──┘    └──┘
typ                     └──┘   └──┘ 
doc                       └──┘     └──┘
 63    le_refl  := λ a, @le_refl ordinal _ _,
id                      └─────┘ └─────┘
src                      └─────┘ └─────┘
typ                     └─────┘ └─────┘
doc                              └─────┘
 64    le_trans := λ a b c, @le_trans ordinal _ _ _ _,
id                        └──────┘ └─────┘
src                          └──────┘ └─────┘
typ                       └──────┘ └─────┘
doc                                   └─────┘
 65    lt_iff_le_not_le := λ a b, @lt_iff_le_not_le ordinal _ _ _ }
id                               └──────────────┘ └─────┘
src                                └──────────────┘ └─────┘
typ                              └──────────────┘ └─────┘
doc                                                 └─────┘
 66  
 67  theorem lt_def {x y : onote} : x < y ↔ repr x < repr y := iff.rfl
id                         └───┘        └──┘   └──┘     └─────┘
src                        └───┘          └──┘    └──┘      └─────┘
typ                        └───┘        └──┘   └──┘     └─────┘
doc                        └───┘            └──┘     └──┘
 68  theorem le_def {x y : onote} : x ≤ y ↔ repr x ≤ repr y := iff.rfl
id                         └───┘        └──┘   └──┘     └─────┘
src                        └───┘          └──┘    └──┘      └─────┘
typ                        └───┘        └──┘   └──┘     └─────┘
doc                        └───┘            └──┘     └──┘
 69  
 70  /-- Convert a `nat` into an ordinal -/
 71  @[simp] def of_nat : ℕ → onote
id                          └───┘
src                          └───┘
typ                         └───┘
doc    └──┘                   └───┘
 72  | 0            := 0
 73  | (nat.succ n) := oadd 0 n.succ_pnat 0
id      └──────┘      └──┘    └────────┘
src     └──────┘       └──┘    └────────┘
typ     └──────┘      └──┘    └────────┘
doc                            └────────┘
 74  
 75  @[simp] theorem of_nat_one : of_nat 1 = 1 := rfl
id                                └────┘         └─┘
src                               └────┘         └─┘
typ                               └────┘         └─┘
doc    └──┘                       └────┘
 76  
 77  @[simp] theorem repr_of_nat (n : ℕ) : repr (of_nat n) = n :=
id                                        └──┘  └────┘    
src                                       └──┘  └────┘    
typ                                       └──┘  └────┘    
doc    └──┘                                └──┘  └────┘
 78  by cases n; simp
id            
src     └────┘   └────
typ     └────┘  └────
doc     └────┘   └────
txt     └────┘   └────
par     └────┘   └────
pid                 
st     └──────────────
 79  
src  
typ  
doc  
txt  
par  
pid  
st   
 80  @[simp] theorem repr_one : repr 1 = 1 :=
id                              └──┘   
src                             └──┘   
typ                             └──┘   
doc    └──┘                     └──┘
 81  by simpa using repr_of_nat 1
id                  └─────────┘
src     └──────────┘└─────────┘└──
typ     └──────────┘└─────────┘└──
doc     └──────────┘           └──
txt     └──────────┘           └──
par     └──────────┘           └──
pid          └────┘           └─
st       └────────────────────────
 82  
src  
typ  
doc  
txt  
par  
pid  
st   
 83  theorem omega_le_oadd (e n a) : ω ^ repr e ≤ repr (oadd e n a) :=
id                                     └──┘   └──┘  └──┘   
src                                    └──┘    └──┘  └──┘
typ                                    └──┘   └──┘  └──┘   
doc                                     └──┘     └──┘
 84  begin
 85    unfold repr,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
 86    refine le_trans _ (le_add_right _ _),
src    └─────┘        └─┘             └───┘
typ    └─────┘        └─┘             └───┘
doc    └─────┘        └─┘             └───┘
txt    └─────┘        └─┘             └───┘
par    └─────┘        └─┘             └───┘
pid                  └─┘             └───┘
 87    simpa using (mul_le_mul_iff_left $ power_pos (repr e) omega_pos).2 (nat_cast_le.2 n.2)
id                                         └──────┘  └──┘   └───────┘     └─────────┘   
src    └──────────┘                      └──────┘ └──┘ └┘└───────┘└──┘ └─────────┘└─┘ └──┘
typ    └──────────┘                      └──────┘ └──┘└┘└───────┘└──┘ └─────────┘└─┘└──┘
doc    └──────────┘                               └──┘ └┘         └──┘            └─┘ └──┘
txt    └──────────┘                                    └┘         └──┘            └─┘ └──┘
par    └──────────┘                                    └┘         └──┘            └─┘ └──┘
pid         └────┘                                    └┘         └──┘            └─┘ └─┘
st                                         └─────────────────────────────────────────────────┘
 88  end
st   └─┘
 89  
 90  theorem oadd_pos (e n a) : 0 < oadd e n a :=
id                                 └──┘   
src                                └──┘
typ                                └──┘   
 91  @lt_of_lt_of_le _ _ _ _ _ (power_pos _ omega_pos)
id    └────────────┘            └───────┘   └───────┘
src   └────────────┘            └───────┘   └───────┘
typ   └────────────┘            └───────┘   └───────┘
 92    (omega_le_oadd _ _ _)
id      └───────────┘
src     └───────────┘
typ     └───────────┘
 93  
 94  /-- Compare ordinal notations -/
 95  def cmp : onote → onote → ordering
id             └───┘  └───┘   └──────┘
src            └───┘  └───┘   └──────┘
typ            └───┘  └───┘   └──────┘
doc            └───┘   └───┘
 96  | 0 0 := ordering.eq
id            └─────────┘
src           └─────────┘
typ           └─────────┘
 97  | _ 0 := ordering.gt
id            └─────────┘
src           └─────────┘
typ           └─────────┘
 98  | 0 _ := ordering.lt
id            └─────────┘
src           └─────────┘
typ           └─────────┘
 99  | o₁@(oadd e₁ n₁ a₁) o₂@(oadd e₂ n₂ a₂) :=
id              └┘ └┘ └┘      └──┘ └┘ └┘ └┘
src                           └──┘
typ             └┘ └┘ └┘      └──┘ └┘ └┘ └┘
100    (cmp e₁ e₂).or_else $ (_root_.cmp (n₁:ℕ) n₂).or_else (cmp a₁ a₂)
id      └─┘       └─────┘     └────────┘          └─────┘   └─┘
src     └─┘       └─────┘     └────────┘          └─────┘   └─┘
typ     └─┘       └─────┘     └────────┘          └─────┘   └─┘
101  
102  theorem eq_of_cmp_eq : ∀ {o₁ o₂}, cmp o₁ o₂ = ordering.eq → o₁ = o₂
id                            └┘ └┘   └─┘ └┘ └┘  └─────────┘   └┘  └┘
src                                    └─┘        └─────────┘      
typ                           └┘ └┘   └─┘ └┘ └┘  └─────────┘   └┘  └┘
doc                                    └─┘
103  | 0            0 h := rfl
id                         └─┘
src                        └─┘
typ                        └─┘
104  | (oadd e n a) 0 h := by injection h
id      └──┘                            
src     └──┘                  └────────┘ 
typ     └──┘                  └────────┘
doc                           └────────┘ 
txt                           └────────┘ 
par                           └────────┘ 
pid                                     
st                           └───────────┘
105  | 0 (oadd e n a) h := by injection h
id        └──┘                          
src       └──┘                └────────┘ 
typ       └──┘                └────────┘
doc                           └────────┘ 
txt                           └────────┘ 
par                           └────────┘ 
pid                                     
st                           └───────────┘
106  | o₁@(oadd e₁ n₁ a₁) o₂@(oadd e₂ n₂ a₂) h := begin
id                            └──┘
src                           └──┘
typ                           └──┘
st                                                └─────
107    revert h, simp [cmp],
id                     └─┘
src    └──────┘  └────┘└─┘
typ    └──────┘  └────┘└─┘
doc    └──────┘  └────┘└─┘
txt    └──────┘  └────┘   
par    └──────┘  └────┘   
pid          └┘         
st   ─────────┘└──────────┘└─
108    cases h₁ : cmp e₁ e₂; intro h; try {cases h},
id                └─┘ └┘ └┘                      
src    └────┘  └─┘└─┘      └─────┘  └───┘└────┘ 
typ    └────┘  └─┘└─┘└┘└┘  └─────┘  └───┘└────┘
doc    └────┘  └─┘└─┘      └─────┘  └───┘└────┘ 
txt    └────┘  └─┘         └─────┘  └───┘└────┘ 
par    └────┘  └─┘         └─────┘  └───┘└────┘ 
pid           └─┘              └┘     └──────┘ 
st   ─────────────────────────────────────┘└─────┘└┘
109    have := eq_of_cmp_eq h₁, subst e₂,
id             └──────────┘ └┘        └┘
src    └──────┘                └────┘
typ    └──────┘└──────────┘└┘  └────┘└┘
doc    └──────┘                └────┘
txt    └──────┘                └────┘
par    └──────┘                └────┘
pid    └───┘└─┘                     
st   ────────────────────────┘└────────┘└─
110    revert h, cases h₂ : _root_.cmp (n₁:ℕ) n₂; intro h; try {cases h},
id                          └────────┘  └┘    └┘                      
src    └──────┘  └────┘  └─┘└────────┘    └┘    └─────┘  └───┘└────┘ 
typ    └──────┘  └────┘  └─┘└────────┘ └┘ └┘└┘  └─────┘  └───┘└────┘
doc    └──────┘  └────┘  └─┘              └┘    └─────┘  └───┘└────┘ 
txt    └──────┘  └────┘  └─┘              └┘    └─────┘  └───┘└────┘ 
par    └──────┘  └────┘  └─┘              └┘    └─────┘  └───┘└────┘ 
pid          └┘         └─┘              └┘         └┘     └──────┘ 
st   ─────────┘└───────────────────────────────────────────────┘└─────┘└┘
111    have := eq_of_cmp_eq h, subst a₂,
id             └──────────┘         └┘
src    └──────┘               └────┘
typ    └──────┘└──────────┘  └────┘└┘
doc    └──────┘               └────┘
txt    └──────┘               └────┘
par    └──────┘               └────┘
pid    └───┘└─┘                    
st   ───────────────────────┘└────────┘└─
112    rw [_root_.cmp, cmp_using_eq_eq] at h₂,
id         └────────┘  └─────────────┘
src    └──┘└────────┘└┘└─────────────┘└─────┘
typ    └──┘└────────┘└┘└─────────────┘└─────┘
doc    └──┘          └┘               └─────┘
txt    └──┘          └┘               └─────┘
par    └──┘          └┘               └─────┘
pid      └┘          └┘               └────┘
st   ───────────────┘└───────────────┘└────┘└─
113    have := subtype.eq (eq_of_incomp h₂), subst n₂, simp
id             └────────┘  └──────────┘ └┘         └┘
src    └──────┘└────────┘ └──────────┘    └────┘    └───┘
typ    └──────┘└────────┘ └──────────┘└┘  └────┘└┘  └───┘
doc    └──────┘                           └────┘    └───┘
txt    └──────┘                           └────┘    └───┘
par    └──────┘                           └────┘    └───┘
pid    └───┘└─┘                                        
st   ─────────────────────────────────────┘└────────┘└─────┘
114  end
st   └─┘
115  
116  theorem zero_lt_one : (0 : onote) < 1 :=
id                              └───┘  
src                             └───┘  
typ                             └───┘  
doc                             └───┘
117  by rw [lt_def, repr, repr_one]; exact zero_lt_one
id          └────┘  └──┘  └──────┘         └─────────┘
src     └──┘└────┘└┘└──┘└┘└──────┘  └────┘└─────────┘
typ     └──┘└────┘└┘└──┘└┘└──────┘  └────┘└─────────┘
doc     └──┘      └┘└──┘└┘          └────┘           
txt     └──┘      └┘    └┘          └────┘           
par     └──┘      └┘    └┘          └────┘           
pid       └┘      └┘    └┘                          
st     └─────────┘└────┘└────────┘└───────────────────
118  
src  
typ  
doc  
txt  
par  
pid  
st   
119  /-- `NF_below o b` says that `o` is a normal form ordinal notation
120    satisfying `repr o < ω ^ b`. -/
121  inductive NF_below : onote → ordinal.{0} → Prop
id                        └───┘   └─────┘
src                       └───┘   └─────┘
typ                       └───┘   └─────┘
doc                       └───┘   └─────┘
122  | zero {b} : NF_below 0 b
id                          
typ                         
123  | oadd' {e n a eb b} : NF_below e eb →
id               └┘     └──────┘  └┘
typ              └┘     └──────┘  └┘
124    NF_below a (repr e) → repr e < b → NF_below (oadd e n a) b
id     └──────┘   └──┘     └──┘                └──┘     
src                └──┘      └──┘                  └──┘
typ    └──────┘   └──┘     └──┘                └──┘     
doc                └──┘      └──┘
125  
126  /-- A normal form ordinal notation has the form
127  
128       ω ^ a₁ * n₁ + ω ^ a₂ * n₂ + ... ω ^ aₖ * nₖ
129    where `a₁ > a₂ > ... > aₖ` and all the `aᵢ` are
130    also in normal form.
131  
132    We will essentially only be interested in normal form
133    ordinal notations, but to avoid complicating the algorithms
134    we define everything over general ordinal notations and
135    only prove correctness with normal form as an invariant. -/
136  @[class] def NF (o : onote) := Exists (NF_below o)
id                        └───┘     └────┘  └──────┘ 
src                       └───┘     └────┘  └──────┘
typ                       └───┘     └────┘  └──────┘ 
doc                       └───┘             └──────┘
137  
138  instance NF.zero : NF 0 := ⟨0, NF_below.zero⟩
id                      └┘          └───────────┘
src                     └┘          └───────────┘
typ                     └┘          └───────────┘
doc                     └┘
139  
140  theorem NF_below.oadd {e n a b} : NF e →
id                                     └┘  
src                                    └┘
typ                                    └┘  
doc                                    └┘
141    NF_below a (repr e) → repr e < b → NF_below (oadd e n a) b
id     └──────┘   └──┘     └──┘      └──────┘  └──┘     
src    └──────┘    └──┘      └──┘        └──────┘  └──┘
typ    └──────┘   └──┘     └──┘      └──────┘  └──┘     
doc    └──────┘    └──┘      └──┘         └──────┘
142  | ⟨eb, h⟩ := NF_below.oadd' h
id               └────────────┘
src               └────────────┘
typ              └────────────┘
143  
144  theorem NF_below.fst {e n a b} (h : NF_below (oadd e n a) b) : NF e :=
id                                       └──────┘  └──┘         └┘ 
src                                      └──────┘  └──┘             └┘
typ                                      └──────┘  └──┘         └┘ 
doc                                      └──────┘                   └┘
145  by cases h with _ _ _ _ eb _ h₁ h₂ h₃; exact ⟨_, h₁⟩
id                                                   └┘
src     └────┘ └─────────────────────────┘  └────┘ └─┘  └─
typ     └────┘└─────────────────────────┘  └────┘ └─┘└┘└─
doc     └────┘ └─────────────────────────┘  └────┘ └─┘  └─
txt     └────┘ └─────────────────────────┘  └────┘ └─┘  └─
par     └────┘ └─────────────────────────┘  └────┘ └─┘  └─
pid           └─────────────────────────┘        └─┘  
st     └──────────────────────────────────────────────────
146  
src  
typ  
doc  
txt  
par  
pid  
st   
147  theorem NF.fst {e n a} : NF (oadd e n a) → NF e
id                            └┘  └──┘      └┘ 
src                           └┘  └──┘          └┘
typ                           └┘  └──┘      └┘ 
doc                           └┘                └┘
148  | ⟨b, h⟩ := h.fst
id               └──┘
src               └──┘
typ              └──┘
149  
150  theorem NF_below.snd {e n a b} (h : NF_below (oadd e n a) b) : NF_below a (repr e) :=
id                                       └──────┘  └──┘         └──────┘   └──┘ 
src                                      └──────┘  └──┘             └──────┘    └──┘
typ                                      └──────┘  └──┘         └──────┘   └──┘ 
doc                                      └──────┘                   └──────┘    └──┘
151  by cases h with _ _ _ _ eb _ h₁ h₂ h₃; exact h₂
id                                               └┘
src     └────┘ └─────────────────────────┘  └────┘  
typ     └────┘└─────────────────────────┘  └────┘└┘
doc     └────┘ └─────────────────────────┘  └────┘  
txt     └────┘ └─────────────────────────┘  └────┘  
par     └────┘ └─────────────────────────┘  └────┘  
pid           └─────────────────────────┘         
st     └─────────────────────────────────────────────
152  
src  
typ  
doc  
txt  
par  
pid  
st   
153  theorem NF.snd' {e n a} : NF (oadd e n a) → NF_below a (repr e)
id                             └┘  └──┘      └──────┘   └──┘ 
src                            └┘  └──┘          └──────┘    └──┘
typ                            └┘  └──┘      └──────┘   └──┘ 
doc                            └┘                └──────┘    └──┘
154  | ⟨b, h⟩ := h.snd
id               └──┘
src               └──┘
typ              └──┘
155  
156  theorem NF.snd {e n a} (h : NF (oadd e n a)) : NF a :=
id                               └┘  └──┘        └┘ 
src                              └┘  └──┘           └┘
typ                              └┘  └──┘        └┘ 
doc                              └┘                 └┘
157  ⟨_, h.snd'⟩
id       └───┘
src       └───┘
typ      └───┘
158  
159  theorem NF.oadd {e a} (h₁ : NF e) (n)
id                               └┘ 
src                              └┘
typ                              └┘ 
doc                              └┘
160    (h₂ : NF_below a (repr e)) : NF (oadd e n a) :=
id           └──────┘   └──┘      └┘  └──┘   
src          └──────┘    └──┘       └┘  └──┘
typ          └──────┘   └──┘      └┘  └──┘   
doc          └──────┘    └──┘       └┘
161  ⟨_, NF_below.oadd h₁ h₂ (ordinal.lt_succ_self _)⟩
id       └───────────┘ └┘ └┘  └──────────────────┘
src      └───────────┘        └──────────────────┘
typ      └───────────┘ └┘ └┘  └──────────────────┘
162  
163  instance NF.oadd_zero (e n) [h : NF e] : NF (oadd e n 0) :=
id                                    └┘     └┘  └──┘  
src                                   └┘      └┘  └──┘
typ                                   └┘     └┘  └──┘  
doc                                   └┘      └┘
164  h.oadd _ NF_below.zero
id   └───┘   └───────────┘
src   └───┘   └───────────┘
typ  └───┘   └───────────┘
165  
166  theorem NF_below.lt {e n a b} (h : NF_below (oadd e n a) b) : repr e < b :=
id                                      └──────┘  └──┘         └──┘   
src                                     └──────┘  └──┘             └──┘   
typ                                     └──────┘  └──┘         └──┘   
doc                                     └──────┘                   └──┘
167  by cases h with _ _ _ _ eb _ h₁ h₂ h₃; exact h₃
id                                               └┘
src     └────┘ └─────────────────────────┘  └────┘  
typ     └────┘└─────────────────────────┘  └────┘└┘
doc     └────┘ └─────────────────────────┘  └────┘  
txt     └────┘ └─────────────────────────┘  └────┘  
par     └────┘ └─────────────────────────┘  └────┘  
pid           └─────────────────────────┘         
st     └─────────────────────────────────────────────
168  
src  
typ  
doc  
txt  
par  
pid  
st   
169  theorem NF_below_zero : ∀ {o}, NF_below o 0 ↔ o = 0
id                                └──────┘      
src                                 └──────┘        
typ                               └──────┘      
doc                                 └──────┘
170  | 0            := ⟨λ _, rfl, λ _, NF_below.zero⟩
id                          └─┘      └───────────┘
src                          └─┘       └───────────┘
typ                         └─┘      └───────────┘
171  | (oadd e n a) := ⟨λ h, (not_le_of_lt h.lt).elim (zero_le _),
id      └──┘                 └──────────┘ └─┘ └──┘   └─────┘
src     └──┘                  └──────────┘  └─┘ └──┘   └─────┘
typ     └──┘                 └──────────┘ └─┘ └──┘   └─────┘
172                     λ e, e.symm ▸ NF_below.zero⟩
id                          └───┘  └───────────┘
src                           └───┘  └───────────┘
typ                         └───┘  └───────────┘
173  
174  theorem NF.zero_of_zero {e n a} (h : NF (oadd e n a)) (e0 : e = 0) : a = 0 :=
id                                        └┘  └──┘                    
src                                       └┘  └──┘                         
typ                                       └┘  └──┘                    
doc                                       └┘
175  by simpa [e0, NF_below_zero] using h.snd'
id             └┘  └───────────┘        └────┘
src     └─────┘  └┘└───────────┘└──────┘└────┘
typ     └─────┘└┘└┘└───────────┘└──────┘└────┘
doc     └─────┘  └┘             └──────┘      
txt     └─────┘  └┘             └──────┘      
par     └─────┘  └┘             └──────┘      
pid            └┘             └────┘      
st     └───────────────────────────────────────
176  
src  
typ  
doc  
txt  
par  
pid  
st   
177  theorem NF_below.repr_lt {o b} (h : NF_below o b) : repr o < ω ^ b :=
id                                       └──────┘      └──┘     
src                                      └──────┘        └──┘     
typ                                      └──────┘      └──┘     
doc                                      └──────┘        └──┘     
178  begin
st   └─────
179    induction h with _ e n a eb b h₁ h₂ h₃ _ IH,
id               
src    └────────┘ └──────────────────────────────┘
typ    └────────┘└──────────────────────────────┘
doc    └────────┘ └──────────────────────────────┘
txt    └────────┘ └──────────────────────────────┘
par    └────────┘ └──────────────────────────────┘
pid              └─────────────────────────────┘
st   ────────────────────────────────────────────┘└─
180    { exact power_pos _ omega_pos },
id             └───────┘   └───────┘
src      └────┘└───────┘└─┘└───────┘
typ      └────┘└───────┘└─┘└───────┘
doc      └────┘         └─┘         
txt      └────┘         └─┘         
par      └────┘         └─┘         
pid                    └─┘         
st   ───┘└──────────────────────────┘└┘
181    { rw repr,
id          └──┘
src      └─┘└──┘
typ      └─┘└──┘
doc      └─┘└──┘
txt      └─┘
par      └─┘
pid        
st   ──────────┘└─
182      refine lt_of_lt_of_le ((ordinal.add_lt_add_iff_left _).2 IH) _,
id              └────────────┘   └─────────────────────────┘      └┘
src      └─────┘└────────────┘  └─────────────────────────┘└────┘  └─┘
typ      └─────┘└────────────┘  └─────────────────────────┘└────┘└┘└─┘
doc      └─────┘                                           └────┘  └─┘
txt      └─────┘                                           └────┘  └─┘
par      └─────┘                                           └────┘  └─┘
pid                                                       └────┘  └─┘
st   ─────────────────────────────────────────────────────────────────┘└─
183      rw ← mul_succ,
id            └──────┘
src      └───┘└──────┘
typ      └───┘└──────┘
doc      └───┘
txt      └───┘
par      └───┘
pid        └─┘
st   ────────────────┘└─
184      refine le_trans (mul_le_mul_left _ $ ordinal.succ_le.2 $ nat_lt_omega _) _,
id              └──────┘  └─────────────┘     └─────────────┘     └──────────┘
src      └─────┘└──────┘ └─────────────┘└─┘ └─────────────┘└─┘ └──────────┘└───┘
typ      └─────┘└──────┘ └─────────────┘└─┘ └─────────────┘└─┘ └──────────┘└───┘
doc      └─────┘                        └─┘                └─┘             └───┘
txt      └─────┘                        └─┘                └─┘             └───┘
par      └─────┘                        └─┘                └─┘             └───┘
pid                                    └─┘                └─┘             └───┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
185      rw ← power_succ,
id            └────────┘
src      └───┘└────────┘
typ      └───┘└────────┘
doc      └───┘
txt      └───┘
par      └───┘
pid        └─┘
st   ──────────────────┘└─
186      exact power_le_power_right omega_pos (ordinal.succ_le.2 h₃) }
id             └──────────────────┘ └───────┘  └─────────────┘   └┘
src      └────┘└──────────────────┘└───────┘ └─────────────┘└─┘  └┘
typ      └────┘└──────────────────┘└───────┘ └─────────────┘└─┘└┘└┘
doc      └────┘                                             └─┘  └┘
txt      └────┘                                             └─┘  └┘
par      └────┘                                             └─┘  └┘
pid                                                        └─┘  
st   ───────────────────────────────────────────────────────────────┘└─
187  end
st   ──┘
188  
189  theorem NF_below.mono {o b₁ b₂} (bb : b₁ ≤ b₂) (h : NF_below o b₁) : NF_below o b₂ :=
id                                         └┘  └┘       └──────┘  └┘    └──────┘  └┘
src                                                     └──────┘         └──────┘
typ                                        └┘  └┘       └──────┘  └┘    └──────┘  └┘
doc                                                      └──────┘         └──────┘
190  begin
st   └─────
191    induction h with _ e n a eb b h₁ h₂ h₃ _ IH; constructor,
id               
src    └────────┘ └──────────────────────────────┘  └─────────┘
typ    └────────┘└──────────────────────────────┘  └─────────┘
doc    └────────┘ └──────────────────────────────┘  └─────────┘
txt    └────────┘ └──────────────────────────────┘  └─────────┘
par    └────────┘ └──────────────────────────────┘  └─────────┘
pid              └─────────────────────────────┘
st   ─────────────────────────────────────────────────────────┘└─
192    exacts [h₁, h₂, lt_of_lt_of_le h₃ bb]
id             └┘  └┘  └────────────┘ └┘ └┘
src    └──────┘  └┘  └┘└────────────┘    └┘
typ    └──────┘└┘└┘└┘└┘└────────────┘└┘└┘└┘
doc    └──────┘  └┘  └┘                  └┘
txt    └──────┘  └┘  └┘                  └┘
par    └──────┘  └┘  └┘                  └┘
pid          └┘  └┘  └┘                  
st   ───────────────────────────────────────┘
193  end
st   └─┘
194  
195  theorem NF.below_of_lt {e n a b} (H : repr e < b) : NF (oadd e n a) → NF_below (oadd e n a) b
id                                         └──┘       └┘  └──┘      └──────┘  └──┘     
src                                        └──┘         └┘  └──┘          └──────┘  └──┘
typ                                        └──┘       └┘  └──┘      └──────┘  └──┘     
doc                                        └──┘          └┘                └──────┘
196  | ⟨b', h⟩ := by cases h with _ _ _ _ eb _ h₁ h₂ h₃;
id                         
src                  └────┘ └─────────────────────────┘
typ                  └────┘└─────────────────────────┘
doc                  └────┘ └─────────────────────────┘
txt                  └────┘ └─────────────────────────┘
par                  └────┘ └─────────────────────────┘
pid                        └─────────────────────────┘
st                  └────────────────────────────────────
197    exact NF_below.oadd' h₁ h₂ H
id           └────────────┘ └┘ └┘ 
src    └────┘└────────────┘     
typ    └────┘└────────────┘└┘└┘
doc    └────┘                   
txt    └────┘                   
par    └────┘                   
pid                            
st   ───────────────────────────────
198  
src  
typ  
doc  
txt  
par  
pid  
st   
199  theorem NF.below_of_lt' : ∀ {o b}, repr o < ω ^ b → NF o → NF_below o b
id                                   └──┘        └┘    └──────┘  
src                                     └──┘          └┘     └──────┘
typ                                  └──┘        └┘    └──────┘  
doc                                     └──┘            └┘     └──────┘
200  | 0            b H _ := NF_below.zero
id                           └───────────┘
src                          └───────────┘
typ                          └───────────┘
201  | (oadd e n a) b H h := h.below_of_lt $ (power_lt_power_iff_right one_lt_omega).1 $
id      └──┘                └──────────┘    └──────────────────────┘ └──────────┘ 
src     └──┘                  └──────────┘    └──────────────────────┘ └──────────┘ 
typ     └──┘                └──────────┘    └──────────────────────┘ └──────────┘ 
202      (lt_of_le_of_lt (omega_le_oadd _ _ _) H)
id        └────────────┘  └───────────┘
src       └────────────┘  └───────────┘
typ       └────────────┘  └───────────┘
203  
204  theorem NF_below_of_nat : ∀ n, NF_below (of_nat n) 1
id                                 └──────┘  └────┘ 
src                                 └──────┘  └────┘
typ                                └──────┘  └────┘ 
doc                                 └──────┘  └────┘
205  | 0            := NF_below.zero
id                     └───────────┘
src                    └───────────┘
typ                    └───────────┘
206  | (nat.succ n) := NF_below.oadd NF.zero NF_below.zero ordinal.zero_lt_one
id      └──────┘       └───────────┘ └─────┘ └───────────┘ └─────────────────┘
src     └──────┘       └───────────┘ └─────┘ └───────────┘ └─────────────────┘
typ     └──────┘       └───────────┘ └─────┘ └───────────┘ └─────────────────┘
207  
208  instance NF_of_nat (n) : NF (of_nat n) := ⟨_, NF_below_of_nat n⟩
id                            └┘  └────┘          └─────────────┘ 
src                           └┘  └────┘           └─────────────┘
typ                           └┘  └────┘          └─────────────┘ 
doc                           └┘  └────┘
209  
210  instance NF_one : NF 1 := by rw ← of_nat_one; apply_instance
id                     └┘              └────────┘
src                    └┘         └───┘└────────┘  └──────────────
typ                    └┘         └───┘└────────┘  └──────────────
doc                    └┘         └───┘            └──────────────
txt                               └───┘            └──────────────
par                               └───┘            └──────────────
pid                                 └─┘                          
st                               └────────────────────────────────
211  
src  
typ  
doc  
txt  
par  
pid  
st   
212  theorem oadd_lt_oadd_1 {e₁ n₁ o₁ e₂ n₂ o₂}
213    (h₁ : NF (oadd e₁ n₁ o₁)) (h₂ : NF (oadd e₂ n₂ o₂))
id           └┘  └──┘ └┘ └┘ └┘         └┘  └──┘ └┘ └┘ └┘
src          └┘  └──┘                  └┘  └──┘
typ          └┘  └──┘ └┘ └┘ └┘         └┘  └──┘ └┘ └┘ └┘
doc          └┘                        └┘
214    (h : e₁ < e₂) : oadd e₁ n₁ o₁ < oadd e₂ n₂ o₂ :=
id          └┘  └┘    └──┘ └┘ └┘ └┘  └──┘ └┘ └┘ └┘
src                   └──┘           └──┘
typ         └┘  └┘    └──┘ └┘ └┘ └┘  └──┘ └┘ └┘ └┘
215  @lt_of_lt_of_le _ _ _ _ _ ((h₁.below_of_lt h).repr_lt) (omega_le_oadd _ _ _)
id    └────────────┘             └┘└──────────┘  └─────┘    └───────────┘
src   └────────────┘               └──────────┘   └─────┘    └───────────┘
typ   └────────────┘             └┘└──────────┘  └─────┘    └───────────┘
216  
217  theorem oadd_lt_oadd_2 {e n₁ o₁ n₂ o₂}
218    (h₁ : NF (oadd e n₁ o₁)) (h₂ : NF (oadd e n₂ o₂))
id           └┘  └──┘  └┘ └┘         └┘  └──┘  └┘ └┘
src          └┘  └──┘                 └┘  └──┘
typ          └┘  └──┘  └┘ └┘         └┘  └──┘  └┘ └┘
doc          └┘                       └┘
219    (h : (n₁:ℕ) < n₂) : oadd e n₁ o₁ < oadd e n₂ o₂ :=
id           └┘    └┘    └──┘  └┘ └┘  └──┘  └┘ └┘
src                      └──┘          └──┘
typ          └┘    └┘    └──┘  └┘ └┘  └──┘  └┘ └┘
220  begin
st   └─────
221    simp [lt_def],
id           └────┘
src    └────┘└────┘
typ    └────┘└────┘
doc    └────┘      
txt    └────┘      
par    └────┘      
pid              
st   ──────────────┘└─
222    refine lt_of_lt_of_le ((ordinal.add_lt_add_iff_left _).2 h₁.snd'.repr_lt)
id            └────────────┘   └─────────────────────────┘      └─────────────┘
src    └─────┘└────────────┘  └─────────────────────────┘└────┘└─────────────┘└─
typ    └─────┘└────────────┘  └─────────────────────────┘└────┘└─────────────┘└─
doc    └─────┘                                           └────┘               └─
txt    └─────┘                                           └────┘               └─
par    └─────┘                                           └────┘               └─
pid                                                     └────┘               └─
st   ────────────────────────────────────────────────────────────────────────────
223      (le_trans _ (le_add_right _ _)),
id        └──────┘    └──────────┘
src  ───┘ └──────┘└─┘ └──────────┘└────┘
typ  ───┘ └──────┘└─┘ └──────────┘└────┘
doc  ───┘         └─┘             └────┘
txt  ───┘         └─┘             └────┘
par  ───┘         └─┘             └────┘
pid  ───┘         └─┘             └────┘
st   ──────────────────────────────────┘└─
224    rwa [← mul_succ, mul_le_mul_iff_left (power_pos _ omega_pos),
id            └──────┘  └─────────────────┘  └───────┘   └───────┘
src    └─────┘└──────┘└┘└─────────────────┘ └───────┘└─┘└───────┘└──
typ    └─────┘└──────┘└┘└─────────────────┘ └───────┘└─┘└───────┘└──
doc    └─────┘        └┘                             └─┘         └──
txt    └─────┘        └┘                             └─┘         └──
par    └─────┘        └┘                             └─┘         └──
pid       └──┘        └┘                             └─┘         └──
st   ────────────────┘└───────────────────────────────────────────┘└─
225         ordinal.succ_le, nat_cast_lt]
id          └─────────────┘  └─────────┘
src  ──────┘└─────────────┘└┘└─────────┘└┘
typ  ──────┘└─────────────┘└┘└─────────┘└┘
doc  ──────┘               └┘           └┘
txt  ──────┘               └┘           └┘
par  ──────┘               └┘           └┘
pid  ──────┘               └┘           
st   ─────────────────────┘└───────────┘
226  end
st   └─┘
227  
228  theorem oadd_lt_oadd_3 {e n a₁ a₂}
229    (h₁ : NF (oadd e n a₁)) (h₂ : NF (oadd e n a₂))
id           └┘  └──┘   └┘         └┘  └──┘   └┘
src          └┘  └──┘                └┘  └──┘
typ          └┘  └──┘   └┘         └┘  └──┘   └┘
doc          └┘                      └┘
230    (h : a₁ < a₂) : oadd e n a₁ < oadd e n a₂ :=
id          └┘  └┘    └──┘   └┘  └──┘   └┘
src                   └──┘         └──┘
typ         └┘  └┘    └──┘   └┘  └──┘   └┘
231  begin
st   └─────
232    rw lt_def, unfold repr,
id        └────┘
src    └─┘└────┘  └─────────┘
typ    └─┘└────┘  └─────────┘
doc    └─┘        └─────────┘
txt    └─┘        └─────────┘
par    └─┘        └─────────┘
pid                    └───┘
st   ──────────┘└───────────┘└─
233    exact (ordinal.add_lt_add_iff_left _).2 h
id            └─────────────────────────┘      
src    └────┘ └─────────────────────────┘└────┘ 
typ    └────┘ └─────────────────────────┘└────┘
doc    └────┘                            └────┘ 
txt    └────┘                            └────┘ 
par    └────┘                            └────┘ 
pid                                     └────┘ 
st   ───────────────────────────────────────────┘
234  end
st   └─┘
235  
236  theorem cmp_compares : ∀ (a b : onote) [NF a] [NF b], (cmp a b).compares a b
id                                  └───┘   └┘    └┘     └─┘   └──────┘   
src                                 └───┘   └┘     └┘      └─┘     └──────┘
typ                                 └───┘   └┘    └┘     └─┘   └──────┘   
doc                                  └───┘   └┘     └┘      └─┘     └──────┘
237  | 0 0 h₁ h₂ := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
238  | (oadd e n a) 0 h₁ h₂ := oadd_pos _ _ _
id      └──┘                   └──────┘
src     └──┘                   └──────┘
typ     └──┘                   └──────┘
239  | 0 (oadd e n a) h₁ h₂ := oadd_pos _ _ _
id        └──┘                 └──────┘
src       └──┘                 └──────┘
typ       └──┘                 └──────┘
240  | o₁@(oadd e₁ n₁ a₁) o₂@(oadd e₂ n₂ a₂) h₁ h₂ := begin
id                            └──┘
src                           └──┘
typ                           └──┘
st                                                    └─────
241      rw cmp,
id          └─┘
src      └─┘└─┘
typ      └─┘└─┘
doc      └─┘└─┘
txt      └─┘
par      └─┘
pid        
st   ─────────┘└─
242      have IHe := @cmp_compares _ _ h₁.fst h₂.fst,
id                    └──────────┘     └────┘ └────┘
src      └──────────┘ └──────────┘└───┘└────┘└────┘
typ      └──────────┘ └──────────┘└───┘└────┘└────┘
doc      └──────────┘             └───┘      
txt      └──────────┘             └───┘      
par      └──────────┘             └───┘      
pid      └──────┘└─┘             └───┘      
st   ──────────────────────────────────────────────┘└─
243      cases cmp e₁ e₂,
id             └─┘ └┘ └┘
src      └────┘└─┘  
typ      └────┘└─┘└┘└┘
doc      └────┘└─┘  
txt      └────┘     
par      └────┘     
pid                
st   ──────────────────┘└─
244      case ordering.lt { exact oadd_lt_oadd_1 h₁ h₂ IHe },
id                                └────────────┘ └┘ └┘ └─┘
src      └─────────────────┘└────┘└────────────┘       
typ      └─────────────────┘└────┘└────────────┘└┘└┘└─┘
doc      └─────────────────┘└────┘                     
txt      └─────────────────┘└────┘                     
par      └─────────────────┘└────┘                     
pid          └──────────┘└──────┘                     └┘
st   ─────────────────────┘└──────────────────────────────┘└┘
245      case ordering.gt { exact oadd_lt_oadd_1 h₂ h₁ IHe },
id                                └────────────┘ └┘ └┘ └─┘
src      └─────────────────┘└────┘└────────────┘       
typ      └─────────────────┘└────┘└────────────┘└┘└┘└─┘
doc      └─────────────────┘└────┘                     
txt      └─────────────────┘└────┘                     
par      └─────────────────┘└────┘                     
pid          └──────────┘└──────┘                     └┘
st   ─────────────────────┘└──────────────────────────────┘└┘
246      change e₁ = e₂ at IHe, subst IHe,
id              └┘  └┘               └─┘
src      └─────┘    └─────┘  └────┘
typ      └─────┘└┘└┘└─────┘  └────┘└─┘
doc      └─────┘     └─────┘  └────┘
txt      └─────┘     └─────┘  └────┘
par      └─────┘     └─────┘  └────┘
pid                 └────┘       
st   ────────────────────────┘└─────────┘└─
247      unfold _root_.cmp, cases nh : cmp_using (<) (n₁:ℕ) n₂,
id                                     └───────┘     └┘    └┘
src      └───────────────┘  └────┘  └─┘└───────┘└─┘    └┘
typ      └───────────────┘  └────┘  └─┘└───────┘└─┘ └┘ └┘└┘
doc      └───────────────┘  └────┘  └─┘          └─┘    └┘
txt      └───────────────┘  └────┘  └─┘          └─┘    └┘
par      └───────────────┘  └────┘  └─┘          └─┘    └┘
pid            └─────────┘         └─┘          └─┘    └┘
st   ────────────────────┘└──────────────────────────────────┘└─
248      case ordering.lt {
src      └──────────────────
typ      └──────────────────
doc      └──────────────────
txt      └──────────────────
par      └──────────────────
pid          └──────────┘└─
st   ─────────────────────┘
249        rw cmp_using_eq_lt at nh, exact oadd_lt_oadd_2 h₁ h₂ nh },
id            └─────────────┘              └────────────┘ └┘ └┘ └┘
src  ─────┘└─┘└─────────────┘└────┘└┘└────┘└────────────┘      
typ  ─────┘└─┘└─────────────┘└────┘└┘└────┘└────────────┘└┘└┘└┘
doc  ─────┘└─┘               └────┘└┘└────┘                    
txt  ─────┘└─┘               └────┘└┘└────┘                    
par  ─────┘└─┘               └────┘└┘└────┘                    
pid  ────────┘               └────────────┘                    └┘
st   ─────────────────────────────┘└──────────────────────────────┘└┘
250      case ordering.gt {
src      └──────────────────
typ      └──────────────────
doc      └──────────────────
txt      └──────────────────
par      └──────────────────
pid          └──────────┘└─
st   ─────────────────────┘
251        rw cmp_using_eq_gt at nh, exact oadd_lt_oadd_2 h₂ h₁ nh },
id            └─────────────┘              └────────────┘ └┘ └┘ └┘
src  ─────┘└─┘└─────────────┘└────┘└┘└────┘└────────────┘      
typ  ─────┘└─┘└─────────────┘└────┘└┘└────┘└────────────┘└┘└┘└┘
doc  ─────┘└─┘               └────┘└┘└────┘                    
txt  ─────┘└─┘               └────┘└┘└────┘                    
par  ─────┘└─┘               └────┘└┘└────┘                    
pid  ────────┘               └────────────┘                    └┘
st   ─────────────────────────────┘└──────────────────────────────┘└┘
252      rw cmp_using_eq_eq at nh,
id          └─────────────┘
src      └─┘└─────────────┘└────┘
typ      └─┘└─────────────┘└────┘
doc      └─┘               └────┘
txt      └─┘               └────┘
par      └─┘               └────┘
pid                       └────┘
st   ───────────────────────────┘└─
253      have := subtype.eq (eq_of_incomp nh), subst n₂,
id               └────────┘  └──────────┘ └┘         └┘
src      └──────┘└────────┘ └──────────┘    └────┘
typ      └──────┘└────────┘ └──────────┘└┘  └────┘└┘
doc      └──────┘                           └────┘
txt      └──────┘                           └────┘
par      └──────┘                           └────┘
pid      └───┘└─┘                                
st   ───────────────────────────────────────┘└────────┘└─
254      have IHa := @cmp_compares _ _ h₁.snd h₂.snd,
id                    └──────────┘     └────┘ └────┘
src      └──────────┘ └──────────┘└───┘└────┘└────┘
typ      └──────────┘ └──────────┘└───┘└────┘└────┘
doc      └──────────┘             └───┘      
txt      └──────────┘             └───┘      
par      └──────────┘             └───┘      
pid      └──────┘└─┘             └───┘      
st   ──────────────────────────────────────────────┘└─
255      cases cmp a₁ a₂,
id             └─┘ └┘ └┘
src      └────┘└─┘  
typ      └────┘└─┘└┘└┘
doc      └────┘└─┘  
txt      └────┘     
par      └────┘     
pid                
st   ──────────────────┘└─
256      case ordering.lt { exact oadd_lt_oadd_3 h₁ h₂ IHa },
id                                └────────────┘ └┘ └┘ └─┘
src      └─────────────────┘└────┘└────────────┘       
typ      └─────────────────┘└────┘└────────────┘└┘└┘└─┘
doc      └─────────────────┘└────┘                     
txt      └─────────────────┘└────┘                     
par      └─────────────────┘└────┘                     
pid          └──────────┘└──────┘                     └┘
st   ─────────────────────┘└──────────────────────────────┘└┘
257      case ordering.gt { exact oadd_lt_oadd_3 h₂ h₁ IHa },
id                                └────────────┘ └┘ └┘ └─┘
src      └─────────────────┘└────┘└────────────┘       
typ      └─────────────────┘└────┘└────────────┘└┘└┘└─┘
doc      └─────────────────┘└────┘                     
txt      └─────────────────┘└────┘                     
par      └─────────────────┘└────┘                     
pid          └──────────┘└──────┘                     └┘
st   ─────────────────────┘└──────────────────────────────┘└┘
258      change a₁ = a₂ at IHa, subst IHa, exact rfl
id              └┘   └┘               └─┘        └─┘
src      └─────┘     └─────┘  └────┘     └────┘└─┘
typ      └─────┘└┘ └┘└─────┘  └────┘└─┘  └────┘└─┘
doc      └─────┘     └─────┘  └────┘     └────┘   
txt      └─────┘     └─────┘  └────┘     └────┘   
par      └─────┘     └─────┘  └────┘     └────┘   
pid                 └────┘                    
st   ────────────────────────┘└─────────┘└───────────
259    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
260  
261  theorem repr_inj {a b} [NF a] [NF b] : repr a = repr b ↔ a = b :=
id                           └┘    └┘     └──┘   └──┘     
src                          └┘     └┘      └──┘    └──┘      
typ                          └┘    └┘     └──┘   └──┘     
doc                          └┘     └┘      └──┘     └──┘
262  ⟨match cmp a b, cmp_compares a b with
id          └─┘    └──────────┘  
src         └─┘      └──────────┘
typ         └─┘    └──────────┘  
doc         └─┘
263   | ordering.lt, (h : repr a < repr b), e := (ne_of_lt h e).elim
id      └─────────┘      └──┘   └──┘         └──────┘     └──┘
src     └─────────┘       └──┘    └──┘           └──────┘     └──┘
typ     └─────────┘      └──┘   └──┘         └──────┘     └──┘
doc                       └──┘     └──┘
264   | ordering.gt, (h : repr a > repr b), e := (ne_of_gt h e).elim
id      └─────────┘      └──┘   └──┘         └──────┘     └──┘
src     └─────────┘       └──┘    └──┘           └──────┘     └──┘
typ     └─────────┘      └──┘   └──┘         └──────┘     └──┘
doc                       └──┘     └──┘
265   | ordering.eq, h, e := h
id      └─────────┘  
src     └─────────┘
typ     └─────────┘  
266   end, congr_arg _⟩
id         └───────┘
src        └───────┘
typ        └───────┘
267  
268  theorem NF.of_dvd_omega_power {b e n a} (h : NF (oadd e n a)) (d : ω ^ b ∣ repr (oadd e n a)) :
id                                                └┘  └──┘               └──┘  └──┘   
src                                               └┘  └──┘                   └──┘  └──┘
typ                                               └┘  └──┘               └──┘  └──┘   
doc                                               └┘                           └──┘
269    b ≤ repr e ∧ ω ^ b ∣ repr a :=
id       └──┘       └──┘ 
src       └──┘         └──┘
typ      └──┘       └──┘ 
doc        └──┘            └──┘
270  begin
st   └─────
271    have := mt repr_inj.1 (λ h, by injection h : oadd e n a ≠ 0),
id             └┘ └──────┘                         └──┘    
src    └──────┘└┘└──────┘└─┘  └──┘  └────────┘ └┘└──┘   └─┘
typ    └──────┘└┘└──────┘└─┘  └──┘  └────────┘└┘└──┘└─┘
doc    └──────┘          └─┘  └──┘  └────────┘ └┘        └─┘
txt    └──────┘          └─┘  └──┘  └────────┘ └┘        └─┘
par    └──────┘          └─┘  └──┘  └────────┘ └┘        └─┘
pid    └───┘└─┘          └─┘  └──┘  └─────────┘ └─┘        └─┘
st   ───────────────────────────────┘└───────────┘└───────────────┘└─
272    have L := le_of_not_lt (λ l, not_le_of_lt (h.below_of_lt l).repr_lt (le_of_dvd this d)),
id               └──────────┘       └──────────┘  └───────────┘             └───────┘ └──┘ 
src    └────────┘└──────────┘  └──┘└──────────┘ └───────────┘ └────────┘ └───────┘     └┘
typ    └────────┘└──────────┘  └──┘└──────────┘ └───────────┘ └────────┘ └───────┘└──┘└┘
doc    └────────┘              └──┘                           └────────┘               └┘
txt    └────────┘              └──┘                           └────────┘               └┘
par    └────────┘              └──┘                           └────────┘               └┘
pid    └────┘└─┘              └──┘                           └────────┘               └┘
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
273    simp at d,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid        └──┘
st   ──────────┘└─
274    exact ⟨L, (dvd_add_iff $ dvd_mul_of_dvd _ $ power_dvd_power _ L).1 d⟩
id                └─────────┘   └────────────┘     └─────────────┘       
src    └────┘  └┘ └─────────┘ └────────────┘└─┘ └─────────────┘└─┘ └──┘ └┘
typ    └────┘  └┘ └─────────┘ └────────────┘└─┘ └─────────────┘└─┘└──┘└┘
doc    └────┘  └┘                           └─┘                └─┘ └──┘ └┘
txt    └────┘  └┘                           └─┘                └─┘ └──┘ └┘
par    └────┘  └┘                           └─┘                └─┘ └──┘ └┘
pid           └┘                           └─┘                └─┘ └──┘ 
st   ───────────────────────────────────────────────────────────────────────┘
275  end
st   └─┘
276  
277  theorem NF.of_dvd_omega {e n a} (h : NF (oadd e n a)) :
id                                        └┘  └──┘   
src                                       └┘  └──┘
typ                                       └┘  └──┘   
doc                                       └┘
278     ω ∣ repr (oadd e n a) → repr e ≠ 0 ∧ ω ∣ repr a :=
id        └──┘  └──┘       └──┘        └──┘ 
src       └──┘  └──┘          └──┘         └──┘
typ       └──┘  └──┘       └──┘        └──┘ 
doc        └──┘                └──┘            └──┘
279  by rw [← power_one ω, ← one_le_iff_ne_zero]; exact h.of_dvd_omega_power
id            └───────┘      └────────────────┘         └──────────────────┘
src     └────┘└───────┘ └──┘└────────────────┘  └────┘└──────────────────┘
typ     └────┘└───────┘ └──┘└────────────────┘  └────┘└──────────────────┘
doc     └────┘          └──┘                    └────┘                    
txt     └────┘          └──┘                    └────┘                    
par     └────┘          └──┘                    └────┘                    
pid       └──┘          └──┘                                             
st     └────────────────┘└────────────────────┘└────────────────────────────
280  
src  
typ  
doc  
txt  
par  
pid  
st   
281  /-- `top_below b o` asserts that the largest exponent in `o`, if
282    it exists, is less than `b`. This is an auxiliary definition
283    for decidability of `NF`. -/
284  def top_below (b) : onote → Prop
id                       └───┘ 
src                      └───┘
typ                      └───┘ 
doc                      └───┘
285  | 0            := true
id                     └──┘
src                    └──┘
typ                    └──┘
286  | (oadd e n a) := cmp e b = ordering.lt
id      └──┘          └─┘     └─────────┘
src     └──┘           └─┘      └─────────┘
typ     └──┘          └─┘     └─────────┘
doc                    └─┘
287  
288  instance decidable_top_below : decidable_rel top_below :=
id                                  └───────────┘ └───────┘
src                                 └───────────┘ └───────┘
typ                                 └───────────┘ └───────┘
doc                                               └───────┘
289  by intros b o; cases o; delta top_below; apply_instance
id                        
src     └────────┘  └────┘   └─────────────┘  └──────────────
typ     └────────┘  └────┘  └─────────────┘  └──────────────
doc     └────────┘  └────┘   └─────────────┘  └──────────────
txt     └────────┘  └────┘   └─────────────┘  └──────────────
par     └────────┘  └────┘   └─────────────┘  └──────────────
pid           └──┘               └────────┘                
st     └─────────────────────────────────────────────────────
290  
src  
typ  
doc  
txt  
par  
pid  
st   
291  theorem NF_below_iff_top_below {b} [NF b] : ∀ {o},
id                                       └┘       
src                                      └┘
typ                                      └┘       
doc                                      └┘
292    NF_below o (repr b) ↔ NF o ∧ top_below b o
id     └──────┘   └──┘    └┘   └───────┘  
src    └──────┘    └──┘     └┘    └───────┘
typ    └──────┘   └──┘    └┘   └───────┘  
doc    └──────┘    └──┘      └┘     └───────┘
293  | 0            := ⟨λ h, ⟨⟨_, h⟩, trivial⟩, λ _, NF_below.zero⟩
id                                  └─────┘       └───────────┘
src                                   └─────┘        └───────────┘
typ                                 └─────┘       └───────────┘
294  | (oadd e n a) :=
id      └──┘
src     └──┘
typ     └──┘
295    ⟨λ h, ⟨⟨_, h⟩, (@cmp_compares _ b h.fst _).eq_lt.2 h.lt⟩,
id                    └──────────┘    └──┘   └───┘   └─┘
src                     └──────────┘      └──┘   └───┘    └─┘
typ                   └──────────┘    └──┘   └───┘   └─┘
296     λ ⟨h₁, h₂⟩, h₁.below_of_lt $ (@cmp_compares _ b h₁.fst _).eq_lt.1 h₂⟩
id        └┘  └┘     └──────────┘     └──────────┘      └──┘   └───┘ 
src                   └──────────┘     └──────────┘       └──┘   └───┘ 
typ       └┘  └┘     └──────────┘     └──────────┘      └──┘   └───┘ 
297  
298  instance decidable_NF : decidable_pred NF
id                           └────────────┘ └┘
src                          └────────────┘ └┘
typ                          └────────────┘ └┘
doc                                         └┘
299  | 0            := is_true NF.zero
id                     └─────┘ └─────┘
src                    └─────┘ └─────┘
typ                    └─────┘ └─────┘
300  | (oadd e n a) := begin
id      └──┘
src     └──┘
typ     └──┘
st                     └─────
301    have := decidable_NF e,
id             └──────────┘ 
src    └──────┘            
typ    └──────┘└──────────┘
doc    └──────┘            
txt    └──────┘            
par    └──────┘            
pid    └───┘└─┘            
st   ───────────────────────┘└─
302    have := decidable_NF a, resetI,
id             └──────────┘ 
src    └──────┘               └────┘
typ    └──────┘└──────────┘  └────┘
doc    └──────┘               └────┘
txt    └──────┘               └────┘
par    └──────┘               └────┘
pid    └───┘└─┘            
st   ───────────────────────┘└─────────
303    apply decidable_of_iff (NF e ∧ NF a ∧ top_below e a),
id           └──────────────┘         └┘     └───────┘  
src    └────┘└──────────────┘     └┘  └───────┘  
typ    └────┘└──────────────┘     └┘  └───────┘
doc    └────┘                     └┘  └───────┘  
txt    └────┘                                    
par    └────┘                                    
pid                                             
st   ─────────────────────────────────────────────────────┘└─
304    abstract {
src    └──────────
typ    └──────────
doc    └──────────
txt    └──────────
par    └──────────
pid            └─
st   ─────────────
305      rw ← and_congr_right (λ h, @NF_below_iff_top_below _ h _),
id            └─────────────┘        └────────────────────┘
src  ───┘└───┘└─────────────┘  └──┘ └────────────────────┘└─┘ └─┘└─
typ  ───┘└───┘└─────────────┘  └──┘ └────────────────────┘└─┘ └─┘└─
doc  ───┘└───┘                 └──┘                       └─┘ └─┘└─
txt  ───┘└───┘                 └──┘                       └─┘ └─┘└─
par  ───┘└───┘                 └──┘                       └─┘ └─┘└─
pid  ────────┘                 └──┘                       └─┘ └────
st   ────────────────────────────────────────────────────────────┘└─
306      exact ⟨λ ⟨h₁, h₂⟩, NF.oadd h₁ n h₂, λ h, ⟨h.fst, h.snd'⟩⟩ },
id                 └┘  └┘   └─────┘                └──┘   └───┘
src  ───┘└────┘  └┘  └┘  └─┘└─────┘     └┘ └──┘  └──┘└┘ └───┘└─┘
typ  ───┘└────┘  └┘└┘└┘└┘└─┘└─────┘    └┘ └──┘  └──┘└┘ └───┘└─┘
doc  ───┘└────┘  └┘  └┘  └─┘            └┘ └──┘      └┘      └─┘
txt  ───┘└────┘  └┘  └┘  └─┘            └┘ └──┘      └┘      └─┘
par  ───┘└────┘  └┘  └┘  └─┘            └┘ └──┘      └┘      └─┘
pid  ─────────┘  └┘  └┘  └─┘            └┘ └──┘      └┘      └──┘
st   ─────────────────────────────────────────────────────────────┘└──
307  end
st   ──┘
308  
309  /-- Addition of ordinal notations (correct only for normal input) -/
310  def add : onote → onote → onote
id             └───┘  └───┘   └───┘
src            └───┘   └───┘   └───┘
typ            └───┘  └───┘   └───┘
doc            └───┘   └───┘   └───┘
311  | 0            o := o
id                  
typ                 
312  | (oadd e n a) o := match add a o with
id      └──┘               └─┘
src     └──┘
typ     └──┘               └─┘
313    | 0 := oadd e n 0
id            └──┘
src           └──┘
typ           └──┘
314    | o'@(oadd e' n' a') := match cmp e e' with
id           └──┘ └┘ └┘ └┘           └─┘
src          └──┘                    └─┘
typ          └──┘ └┘ └┘ └┘           └─┘
doc                                  └─┘
315      | ordering.lt := o'
id         └─────────┘
src        └─────────┘
typ        └─────────┘
316      | ordering.eq := oadd e (n + n') a'
id         └─────────┘    └──┘      
src        └─────────┘    └──┘      
typ        └─────────┘    └──┘      
317      | ordering.gt := oadd e n o'
id         └─────────┘    └──┘
src        └─────────┘    └──┘
typ        └─────────┘    └──┘
318      end
319    end
320  
321  instance : has_add onote := ⟨add⟩
id              └─────┘ └───┘     └─┘
src             └─────┘ └───┘     └─┘
typ             └─────┘ └───┘     └─┘
doc                     └───┘     └─┘
322  
323  @[simp] theorem zero_add (o : onote) : 0 + o = o := rfl
id                                 └───┘             └─┘
src                                └───┘               └─┘
typ                                └───┘             └─┘
doc    └──┘                        └───┘
324  theorem oadd_add (e n a o) : oadd e n a + o = add._match_1 e n (a + o) := rfl
id                                └──┘       └──────────┘           └─┘
src                               └──┘           └──────────┘               └─┘
typ                               └──┘       └──────────┘           └─┘
325  
326  /-- Subtraction of ordinal notations (correct only for normal input) -/
327  def sub : onote → onote → onote
id             └───┘  └───┘   └───┘
src            └───┘   └───┘   └───┘
typ            └───┘  └───┘   └───┘
doc            └───┘   └───┘   └───┘
328  | 0 o := 0
329  | o 0 := o
id     
typ    
330  | o₁@(oadd e₁ n₁ a₁) (oadd e₂ n₂ a₂) := match cmp e₁ e₂ with
id              └┘ └┘ └┘   └──┘ └┘ └┘ └┘           └─┘
src                        └──┘                    └─┘
typ             └┘ └┘ └┘   └──┘ └┘ └┘ └┘           └─┘
doc                                                └─┘
331    | ordering.lt := 0
id       └─────────┘
src      └─────────┘
typ      └─────────┘
332    | ordering.gt := o₁
id       └─────────┘
src      └─────────┘
typ      └─────────┘
333    | ordering.eq := match (n₁:ℕ) - n₂ with
id       └─────────┘                
src      └─────────┘                
typ      └─────────┘                
334      | 0            := if n₁ = n₂ then sub a₁ a₂ else 0
id                                        └─┘
src                              
typ                                       └─┘
335      | (nat.succ k) := oadd e₁ k.succ_pnat a₁
id          └──────┘      └──┘     └────────┘
src         └──────┘       └──┘     └────────┘
typ         └──────┘      └──┘     └────────┘
doc                                 └────────┘
336    end
337  end
338  
339  instance : has_sub onote := ⟨sub⟩
id              └─────┘ └───┘     └─┘
src             └─────┘ └───┘     └─┘
typ             └─────┘ └───┘     └─┘
doc                     └───┘     └─┘
340  
341  theorem add_NF_below {b} : ∀ {o₁ o₂}, NF_below o₁ b → NF_below o₂ b → NF_below (o₁ + o₂) b
id                                └┘ └┘   └──────┘ └┘    └──────┘ └┘    └──────┘  └┘  └┘  
src                                        └──────┘        └──────┘        └──────┘     
typ                               └┘ └┘   └──────┘ └┘    └──────┘ └┘    └──────┘  └┘  └┘  
doc                                        └──────┘        └──────┘        └──────┘
342  | 0            o h₁ h₂ := h₂
id                       └┘
typ                      └┘
343  | (oadd e n a) o h₁ h₂ := begin
id      └──┘
src     └──┘
typ     └──┘
st                             └─────
344    have h' := add_NF_below (h₁.snd.mono $ le_of_lt h₁.lt) h₂,
id                └──────────┘  └─────────┘   └──────┘ └───┘  └┘
src    └─────────┘             └─────────┘ └──────┘└───┘└┘
typ    └─────────┘└──────────┘ └─────────┘ └──────┘└───┘└┘└┘
doc    └─────────┘                                      └┘
txt    └─────────┘                                      └┘
par    └─────────┘                                      └┘
pid    └─────┘└─┘                                      └┘
st   ──────────────────────────────────────────────────────────┘└─
345    simp [oadd_add], cases a + o with e' n' a',
id           └──────┘           
src    └────┘└──────┘  └────┘  └────────────┘
typ    └────┘└──────┘  └────┘└────────────┘
doc    └────┘          └────┘   └────────────┘
txt    └────┘          └────┘   └────────────┘
par    └────┘          └────┘   └────────────┘
pid                          └────────────┘
st   ────────────────┘└─────────────────────────┘└─
346    { exact NF_below.oadd h₁.fst NF_below.zero h₁.lt },
id             └───────────┘ └────┘ └───────────┘ └───┘
src      └────┘└───────────┘└────┘└───────────┘└───┘
typ      └────┘└───────────┘└────┘└───────────┘└───┘
doc      └────┘                                     
txt      └────┘                                     
par      └────┘                                     
pid                                                
st   ───┘└─────────────────────────────────────────────┘└┘
347    simp [add], have := @cmp_compares _ _ h₁.fst h'.fst,
id           └─┘            └──────────┘     └────┘ └────┘
src    └────┘└─┘  └──────┘ └──────────┘└───┘└────┘└────┘
typ    └────┘└─┘  └──────┘ └──────────┘└───┘└────┘└────┘
doc    └────┘└─┘  └──────┘             └───┘      
txt    └────┘     └──────┘             └───┘      
par    └────┘     └──────┘             └───┘      
pid             └───┘└─┘             └───┘      
st   ───────────┘└───────────────────────────────────────┘└─
348    cases cmp e e'; simp [add],
id           └─┘  └┘        └─┘
src    └────┘└─┘     └────┘└─┘
typ    └────┘└─┘└┘  └────┘└─┘
doc    └────┘└─┘     └────┘└─┘
txt    └────┘        └────┘   
par    └────┘        └────┘   
pid                        
st   ───────────────────────────┘└─
349    { exact h' },
id             └┘
src      └────┘  
typ      └────┘└┘
doc      └────┘  
txt      └────┘  
par      └────┘  
pid             
st   ───┘└───────┘└┘
350    { simp at this, subst e',
id                           └┘
src      └──────────┘  └────┘
typ      └──────────┘  └────┘└┘
doc      └──────────┘  └────┘
txt      └──────────┘  └────┘
par      └──────────┘  └────┘
pid          └─────┘       
st   ───┘└──────────┘└────────┘└─
351      exact NF_below.oadd h'.fst h'.snd h'.lt },
id             └───────────┘ └────┘ └────┘ └───┘
src      └────┘└───────────┘└────┘└────┘└───┘
typ      └────┘└───────────┘└────┘└────┘└───┘
doc      └────┘                              
txt      └────┘                              
par      └────┘                              
pid                                         
st   ───────────────────────────────────────────┘└┘
352    { exact NF_below.oadd h₁.fst (NF.below_of_lt this ⟨_, h'⟩) h₁.lt }
id             └───────────┘ └────┘  └────────────┘ └──┘     └┘   └───┘
src      └────┘└───────────┘└────┘ └────────────┘     └─┘  └─┘└───┘
typ      └────┘└───────────┘└────┘ └────────────┘└──┘ └─┘└┘└─┘└───┘
doc      └────┘                                       └─┘  └─┘     
txt      └────┘                                       └─┘  └─┘     
par      └────┘                                       └─┘  └─┘     
pid                                                  └─┘  └─┘     
st   ──────────────────────────────────────────────────────────────────┘└─
353  end
st   ──┘
354  
355  instance add_NF (o₁ o₂) : ∀ [NF o₁] [NF o₂], NF (o₁ + o₂)
id                               └┘ └┘   └┘ └┘   └┘  └┘  └┘
src                               └┘      └┘      └┘     
typ                              └┘ └┘   └┘ └┘   └┘  └┘  └┘
doc                               └┘      └┘      └┘
356  | ⟨b₁, h₁⟩ ⟨b₂, h₂⟩ := (b₁.le_total b₂).elim
id      └┘  └┘   └┘  └┘        └───────┘    └──┘
src                            └───────┘    └──┘
typ     └┘  └┘   └┘  └┘        └───────┘    └──┘
357    (λ h, ⟨b₂, add_NF_below (h₁.mono h) h₂⟩)
id               └──────────┘    └───┘ 
src               └──────────┘    └───┘
typ              └──────────┘    └───┘ 
358    (λ h, ⟨b₁, add_NF_below h₁ (h₂.mono h)⟩)
id               └──────────┘       └───┘ 
src               └──────────┘       └───┘
typ              └──────────┘       └───┘ 
359  
360  @[simp] theorem repr_add : ∀ o₁ o₂ [NF o₁] [NF o₂], repr (o₁ + o₂) = repr o₁ + repr o₂
id                                └┘ └┘  └┘ └┘   └┘ └┘   └──┘  └┘  └┘   └──┘ └┘  └──┘ └┘
src                                      └┘      └┘      └──┘           └──┘     └──┘
typ                               └┘ └┘  └┘ └┘   └┘ └┘   └──┘  └┘  └┘   └──┘ └┘  └──┘ └┘
doc    └──┘                              └┘      └┘      └──┘             └──┘      └──┘
361  | 0            o h₁ h₂ := by simp
src                               └───┘
typ                               └───┘
doc                               └───┘
txt                               └───┘
par                               └───┘
pid                                   
st                               └────┘
362  | (oadd e n a) o h₁ h₂ := begin
id      └──┘
src     └──┘
typ     └──┘
st                             └─────
363    haveI := h₁.snd, have h' := repr_add a o,
id              └────┘             └──────┘  
src    └───────┘└────┘  └─────────┘         
typ    └───────┘└────┘  └─────────┘└──────┘
doc    └───────┘        └─────────┘         
txt    └───────┘        └─────────┘         
par    └───────┘        └─────────┘         
pid         └─┘        └─────┘└─┘         
st   ────────────────┘└───────────────────────┘└─
364    conv at h' in (_+o) {simp [(+)]},
id                     
src    └────────────┘  └─┘└────┘ └─┘
typ    └────────────┘ └─┘└────┘ └─┘
txt    └────────────┘   └─┘└────┘ └─┘
par    └────────────┘   └─┘└────┘ └─┘
pid        └────┘└──┘   └──────┘ └──┘
st   ──────────────────────┘└────────┘└┘
365    have nf := onote.add_NF a o,
id                └──────────┘  
src    └─────────┘└──────────┘ 
typ    └─────────┘└──────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid    └─────┘└─┘             
st   ────────────────────────────┘└─
366    conv at nf in (_+o) {simp [(+)]},
id                      
src    └────────────┘   └─┘└────┘ └─┘
typ    └────────────┘  └─┘└────┘ └─┘
txt    └────────────┘   └─┘└────┘ └─┘
par    └────────────┘   └─┘└────┘ └─┘
pid        └────┘└──┘   └──────┘ └──┘
st   ──────────────────────┘└────────┘└┘
367    conv in (_+o) {simp [(+), add]},
id                              └─┘
src    └──────┘   └─┘└────┘ └──┘└─┘
typ    └──────┘  └─┘└────┘ └──┘└─┘
doc                              └─┘
txt    └──────┘   └─┘└────┘ └──┘   
par    └──────┘   └─┘└────┘ └──┘   
pid        └─┘   └──────┘ └──┘   └┘
st   ────────────────┘└─────────────┘└┘
368    cases add a o with e' n' a'; simp [add, h'.symm],
id           └─┘                        └─┘
src    └────┘└─┘  └────────────┘  └────┘└─┘└┘       
typ    └────┘└─┘└────────────┘  └────┘└─┘└┘└─────┘
doc    └────┘└─┘  └────────────┘  └────┘└─┘└┘       
txt    └────┘     └────────────┘  └────┘   └┘       
par    └────┘     └────────────┘  └────┘   └┘       
pid              └────────────┘         └┘       
st   ─────────────────────────────────────────────────┘└─
369    have := h₁.fst, have := nf.fst, have ee := cmp_compares e e',
id             └────┘          └────┘             └──────────┘  └┘
src    └──────┘└────┘  └──────┘└────┘  └─────────┘└──────────┘ 
typ    └──────┘└────┘  └──────┘└────┘  └─────────┘└──────────┘└┘
doc    └──────┘        └──────┘        └─────────┘             
txt    └──────┘        └──────┘        └─────────┘             
par    └──────┘        └──────┘        └─────────┘             
pid    └───┘└─┘        └───┘└─┘        └─────┘└─┘             
st   ───────────────┘└──────────────┘└────────────────────────────┘└─
370    cases cmp e e'; simp [add],
id           └─┘  └┘        └─┘
src    └────┘└─┘     └────┘└─┘
typ    └────┘└─┘└┘  └────┘└─┘
doc    └────┘└─┘     └────┘└─┘
txt    └────┘        └────┘   
par    └────┘        └────┘   
pid                        
st   ───────────────────────────┘└─
371    { rw [← add_assoc, @add_absorp _ (repr e') (ω ^ repr e' * (n':ℕ))],
id             └───────┘   └────────┘                 └──┘ └┘   └┘
src      └────┘└───────┘└┘ └────────┘└─┘       └┘  └──┘      └─┘
typ      └────┘└───────┘└┘ └────────┘└─┘       └┘  └──┘└┘ └┘ └─┘
doc      └────┘         └┘           └─┘       └┘   └──┘       └─┘
txt      └────┘         └┘           └─┘       └┘              └─┘
par      └────┘         └┘           └─┘       └┘              └─┘
pid        └──┘         └┘           └─┘       └┘              └─┘
st   ───┘└─────────────┘└──────────────────────────────────────────────┘└─
372      { have := (h₁.below_of_lt ee).repr_lt, unfold repr at this,
id                  └────────────┘ └┘
src        └──────┘ └────────────┘  └───────┘  └─────────────────┘
typ        └──────┘ └────────────┘└┘└───────┘  └─────────────────┘
doc        └──────┘                 └───────┘  └─────────────────┘
txt        └──────┘                 └───────┘  └─────────────────┘
par        └──────┘                 └───────┘  └─────────────────┘
pid        └───┘└─┘                 └──────┘        └───┘└──────┘
st   ─────┘└─────────────────────────────────┘└───────────────────┘└─
373        exact lt_of_le_of_lt (le_add_right _ _) this },
id               └────────────┘  └──────────┘      └──┘
src        └────┘└────────────┘ └──────────┘└────┘    
typ        └────┘└────────────┘ └──────────┘└────┘└──┘
doc        └────┘                           └────┘    
txt        └────┘                           └────┘    
par        └────┘                           └────┘    
pid                                        └────┘    
st   ──────────────────────────────────────────────────┘└┘
374      { simpa using (mul_le_mul_iff_left $
id                      └─────────────────┘
src        └──────────┘ └─────────────────┘ 
typ        └──────────┘ └─────────────────┘ 
doc        └──────────┘                     
txt        └──────────┘                     
par        └──────────┘                     
pid             └────┘                     
st   ─────────────────────────────────────────
375          power_pos (repr e') omega_pos).2 (nat_cast_le.2 n'.pos) } },
id           └───────┘  └──┘ └┘  └───────┘     └─────────┘   └────┘
src  ───────┘└───────┘ └──┘  └┘└───────┘└──┘ └─────────┘└─┘└────┘└┘
typ  ───────┘└───────┘ └──┘└┘└┘└───────┘└──┘ └─────────┘└─┘└────┘└┘
doc  ───────┘          └──┘  └┘         └──┘            └─┘      └┘
txt  ───────┘                └┘         └──┘            └─┘      └┘
par  ───────┘                └┘         └──┘            └─┘      └┘
pid  ───────┘                └┘         └──┘            └─┘      
st   ───────────────────────────────────────────────────────────────┘└──┘
376    { change e = e' at ee, subst e',
id                └┘              └┘
src      └─────┘   └────┘  └────┘
typ      └─────┘└┘└────┘  └────┘└┘
doc      └─────┘    └────┘  └────┘
txt      └─────┘    └────┘  └────┘
par      └─────┘    └────┘  └────┘
pid                └───┘       
st   ──────────────────────┘└────────┘└─
377      rw [← add_assoc, ← ordinal.mul_add, ← nat.cast_add] }
id             └───────┘    └─────────────┘    └──────────┘
src      └────┘└───────┘└──┘└─────────────┘└──┘└──────────┘└┘
typ      └────┘└───────┘└──┘└─────────────┘└──┘└──────────┘└┘
doc      └────┘         └──┘               └──┘            └┘
txt      └────┘         └──┘               └──┘            └┘
par      └────┘         └──┘               └──┘            └┘
pid        └──┘         └──┘               └──┘            
st   ──────────────────┘└─────────────────┘└──────────────┘└─
378  end
st   ──┘
379  
380  theorem sub_NF_below : ∀ {o₁ o₂ b}, NF_below o₁ b → NF o₂ → NF_below (o₁ - o₂) b
id                            └┘ └┘    └──────┘ └┘    └┘ └┘   └──────┘  └┘  └┘  
src                                      └──────┘        └┘      └──────┘     
typ                           └┘ └┘    └──────┘ └┘    └┘ └┘   └──────┘  └┘  └┘  
doc                                      └──────┘        └┘      └──────┘
381  | 0            o b h₁ h₂ := by cases o; exact NF_below.zero
id                                                └───────────┘
src                                 └────┘   └────┘└───────────┘
typ                                 └────┘  └────┘└───────────┘
doc                                 └────┘   └────┘             
txt                                 └────┘   └────┘             
par                                 └────┘   └────┘             
pid                                                           
st                                 └────────────────────────────┘
382  | (oadd e n a) 0 b h₁ h₂ := h₁
id      └──┘            └┘
src     └──┘
typ     └──┘            └┘
383  | (oadd e₁ n₁ a₁) (oadd e₂ n₂ a₂) b h₁ h₂ := begin
id                      └──┘
src                     └──┘
typ                     └──┘
st                                                └─────
384    have h' := sub_NF_below h₁.snd h₂.snd,
id                └──────────┘ └────┘ └────┘
src    └─────────┘            └────┘└────┘
typ    └─────────┘└──────────┘└────┘└────┘
doc    └─────────┘                  
txt    └─────────┘                  
par    └─────────┘                  
pid    └─────┘└─┘                  
st   ──────────────────────────────────────┘└─
385    simp [has_sub.sub, sub] at h' ⊢,
id                        └─┘
src    └────┘           └┘└─┘└───────┘
typ    └────┘           └┘└─┘└───────┘
doc    └────┘           └┘└─┘└───────┘
txt    └────┘           └┘   └───────┘
par    └────┘           └┘   └───────┘
pid                   └┘   └─────┘
st   ────────────────────────────────┘└─
386    have := @cmp_compares _ _ h₁.fst h₂.fst,
id              └──────────┘     └────┘ └────┘
src    └──────┘ └──────────┘└───┘└────┘└────┘
typ    └──────┘ └──────────┘└───┘└────┘└────┘
doc    └──────┘             └───┘      
txt    └──────┘             └───┘      
par    └──────┘             └───┘      
pid    └───┘└─┘             └───┘      
st   ────────────────────────────────────────┘└─
387    cases cmp e₁ e₂; simp [sub],
id           └─┘ └┘ └┘        └─┘
src    └────┘└─┘      └────┘└─┘
typ    └────┘└─┘└┘└┘  └────┘└─┘
doc    └────┘└─┘      └────┘└─┘
txt    └────┘         └────┘   
par    └────┘         └────┘   
pid                         
st   ────────────────────────────┘└─
388    { apply NF_below.zero },
id             └───────────┘
src      └────┘└───────────┘
typ      └────┘└───────────┘
doc      └────┘             
txt      └────┘             
par      └────┘             
pid                        
st   ───┘└──────────────────┘└┘
389    { simp at this, subst e₂,
id                           └┘
src      └──────────┘  └────┘
typ      └──────────┘  └────┘└┘
doc      └──────────┘  └────┘
txt      └──────────┘  └────┘
par      └──────────┘  └────┘
pid          └─────┘       
st   ───┘└──────────┘└────────┘└─
390      cases mn : (n₁:ℕ) - n₂; simp [sub],
id                   └┘     └┘        └─┘
src      └────┘  └─┘    └┘    └────┘└─┘
typ      └────┘  └─┘ └┘ └┘└┘  └────┘└─┘
doc      └────┘  └─┘    └┘     └────┘└─┘
txt      └────┘  └─┘    └┘     └────┘   
par      └────┘  └─┘    └┘     └────┘   
pid             └─┘    └┘            
st   ─────────────────────────────────────┘└─
391      { by_cases en : n₁ = n₂; simp [en],
id                       └┘   └┘        └┘
src        └───────┘  └─┘       └────┘  
typ        └───────┘  └─┘└┘ └┘  └────┘└┘
doc        └───────┘  └─┘       └────┘  
txt        └───────┘  └─┘       └────┘  
par        └───────┘  └─┘       └────┘  
pid                  └─┘             
st   ─────┘└──────────────────────────────┘└─
392        { exact h'.mono (le_of_lt h₁.lt) },
id                 └─────┘  └──────┘ └───┘
src          └────┘└─────┘ └──────┘└───┘└┘
typ          └────┘└─────┘ └──────┘└───┘└┘
doc          └────┘                     └┘
txt          └────┘                     └┘
par          └────┘                     └┘
pid                                    
st   ───────┘└─────────────────────────────┘└┘
393        { exact NF_below.zero } },
id                 └───────────┘
src          └────┘└───────────┘
typ          └────┘└───────────┘
doc          └────┘             
txt          └────┘             
par          └────┘             
pid                            
st   ───────────────────────────┘└──┘
394      { exact NF_below.oadd h₁.fst h₁.snd h₁.lt } },
id               └───────────┘ └────┘ └────┘ └───┘
src        └────┘└───────────┘└────┘└────┘└───┘
typ        └────┘└───────────┘└────┘└────┘└───┘
doc        └────┘                              
txt        └────┘                              
par        └────┘                              
pid                                           
st   ─────────────────────────────────────────────┘└──┘
395    { exact h₁ }
id             └┘
src      └────┘  
typ      └────┘└┘
doc      └────┘  
txt      └────┘  
par      └────┘  
pid             
st   ────────────┘└─
396  end
st   ──┘
397  
398  instance sub_NF (o₁ o₂) : ∀ [NF o₁] [NF o₂], NF (o₁ - o₂)
id                               └┘ └┘   └┘ └┘   └┘  └┘  └┘
src                               └┘      └┘      └┘     
typ                              └┘ └┘   └┘ └┘   └┘  └┘  └┘
doc                               └┘      └┘      └┘
399  | ⟨b₁, h₁⟩ h₂ := ⟨b₁, sub_NF_below h₁ h₂⟩
id      └┘  └┘  └┘         └──────────┘
src                        └──────────┘
typ     └┘  └┘  └┘         └──────────┘
400  
401  @[simp] theorem repr_sub : ∀ o₁ o₂ [NF o₁] [NF o₂], repr (o₁ - o₂) = repr o₁ - repr o₂
id                                └┘ └┘  └┘ └┘   └┘ └┘   └──┘  └┘  └┘   └──┘ └┘  └──┘ └┘
src                                      └┘      └┘      └──┘           └──┘     └──┘
typ                               └┘ └┘  └┘ └┘   └┘ └┘   └──┘  └┘  └┘   └──┘ └┘  └──┘ └┘
doc    └──┘                              └┘      └┘      └──┘             └──┘      └──┘
402  | 0            o h₁ h₂ := by cases o; exact (ordinal.zero_sub _).symm
id                                               └──────────────┘
src                               └────┘   └────┘ └──────────────┘└───────┘
typ                               └────┘  └────┘ └──────────────┘└───────┘
doc                               └────┘   └────┘                 └───────┘
txt                               └────┘   └────┘                 └───────┘
par                               └────┘   └────┘                 └───────┘
pid                                                             └─────┘└┘
st                               └────────────────────────────────────────┘
403  | (oadd e n a) 0 h₁ h₂ := (ordinal.sub_zero _).symm
id      └──┘                    └──────────────┘   └──┘
src     └──┘                    └──────────────┘   └──┘
typ     └──┘                    └──────────────┘   └──┘
404  | (oadd e₁ n₁ a₁) (oadd e₂ n₂ a₂) h₁ h₂ := begin
id                      └──┘
src                     └──┘
typ                     └──┘
st                                              └─────
405    haveI := h₁.snd, haveI := h₂.snd, have h' := repr_sub a₁ a₂,
id              └────┘           └────┘             └──────┘ └┘ └┘
src    └───────┘└────┘  └───────┘└────┘  └─────────┘          
typ    └───────┘└────┘  └───────┘└────┘  └─────────┘└──────┘└┘└┘
doc    └───────┘        └───────┘        └─────────┘          
txt    └───────┘        └───────┘        └─────────┘          
par    └───────┘        └───────┘        └─────────┘          
pid         └─┘             └─┘        └─────┘└─┘          
st   ────────────────┘└───────────────┘└─────────────────────────┘└─
406    conv at h' in (a₁-a₂) {simp [has_sub.sub]},
id                    └┘└┘
src    └────────────┘     └─┘└────┘           
typ    └────────────┘ └┘└┘└─┘└────┘           
txt    └────────────┘      └─┘└────┘           
par    └────────────┘      └─┘└────┘           
pid        └────┘└──┘      └──────┘           └┘
st   ────────────────────────┘└────────────────┘└┘
407    have nf := onote.sub_NF a₁ a₂,
id                └──────────┘ └┘ └┘
src    └─────────┘└──────────┘  
typ    └─────────┘└──────────┘└┘└┘
doc    └─────────┘              
txt    └─────────┘              
par    └─────────┘              
pid    └─────┘└─┘              
st   ──────────────────────────────┘└─
408    conv at nf in (a₁-a₂) {simp [has_sub.sub]},
id                    └┘ └┘
src    └────────────┘      └─┘└────┘           
typ    └────────────┘ └┘ └┘└─┘└────┘           
txt    └────────────┘      └─┘└────┘           
par    └────────────┘      └─┘└────┘           
pid        └────┘└──┘      └──────┘           └┘
st   ────────────────────────┘└────────────────┘└┘
409    conv in (_-oadd _ _ _) {simp [has_sub.sub, sub]},
id                └──┘                            └─┘
src    └──────┘  └──┘└───────┘└────┘           └┘└─┘
typ    └──────┘  └──┘└───────┘└────┘           └┘└─┘
doc                                               └─┘
txt    └──────┘      └───────┘└────┘           └┘   
par    └──────┘      └───────┘└────┘           └┘   
pid        └─┘      └─────┘└──────┘           └┘   └┘
st   ─────────────────────────┘└─────────────────────┘└┘
410    have ee := @cmp_compares _ _ h₁.fst h₂.fst,
id                 └──────────┘     └────┘ └────┘
src    └─────────┘ └──────────┘└───┘└────┘└────┘
typ    └─────────┘ └──────────┘└───┘└────┘└────┘
doc    └─────────┘             └───┘      
txt    └─────────┘             └───┘      
par    └─────────┘             └───┘      
pid    └─────┘└─┘             └───┘      
st   ───────────────────────────────────────────┘└─
411    cases cmp e₁ e₂,
id           └─┘ └┘ └┘
src    └────┘└─┘  
typ    └────┘└─┘└┘└┘
doc    └────┘└─┘  
txt    └────┘     
par    └────┘     
pid              
st   ────────────────┘└─
412    { rw [sub_eq_zero_iff_le.2], {refl},
id           └────────────────┘
src      └──┘└────────────────┘└─┘   └──┘
typ      └──┘└────────────────┘└─┘   └──┘
doc      └──┘                  └─┘   └──┘
txt      └──┘                  └─┘   └──┘
par      └──┘                  └─┘   └──┘
pid        └┘                  └─┘
st   ───┘└────────────────────┘└─┘└─────┘└┘
413      exact le_of_lt (oadd_lt_oadd_1 h₁ h₂ ee) },
id             └──────┘  └────────────┘ └┘ └┘ └┘
src      └────┘└──────┘ └────────────┘      └┘
typ      └────┘└──────┘ └────────────┘└┘└┘└┘└┘
doc      └────┘                             └┘
txt      └────┘                             └┘
par      └────┘                             └┘
pid                                        
st   ────────────────────────────────────────────┘└┘
414    { change e₁ = e₂ at ee, subst e₂, unfold sub._match_1,
id              └┘  └┘              └┘
src      └─────┘    └────┘  └────┘    └─────────────────┘
typ      └─────┘└┘└┘└────┘  └────┘└┘  └─────────────────┘
doc      └─────┘     └────┘  └────┘    └─────────────────┘
txt      └─────┘     └────┘  └────┘    └─────────────────┘
par      └─────┘     └────┘  └────┘    └─────────────────┘
pid                 └───┘                 └───────────┘
st   ───┘└──────────────────┘└────────┘└───────────────────┘└─
415      cases mn : (n₁:ℕ) - n₂; dsimp only [sub._match_2],
id                   └┘      └┘              └──────────┘
src      └────┘  └─┘    └┘     └──────────┘└──────────┘
typ      └────┘  └─┘ └┘ └┘ └┘  └──────────┘└──────────┘
doc      └────┘  └─┘    └┘     └──────────┘            
txt      └────┘  └─┘    └┘     └──────────┘            
par      └────┘  └─┘    └┘     └──────────┘            
pid             └─┘    └┘          └───┘└┘            
st   ────────────────────────────────────────────────────┘└─
416      { by_cases en : n₁ = n₂,
id                       └┘   └┘
src        └───────┘  └─┘   
typ        └───────┘  └─┘└┘ └┘
doc        └───────┘  └─┘   
txt        └───────┘  └─┘   
par        └───────┘  └─┘   
pid                  └─┘   
st   ─────┘└───────────────────┘└─
417        { simp [en], rwa [add_sub_add_cancel] },
id                 └┘        └────────────────┘
src          └────┘    └───┘└────────────────┘└┘
typ          └────┘└┘  └───┘└────────────────┘└┘
doc          └────┘    └───┘                  └┘
txt          └────┘    └───┘                  └┘
par          └────┘    └───┘                  └┘
pid                     └┘                  
st   ───────┘└───────┘└───────────────────────┘└┘
418        { simp [en, -repr],
id                 └┘
src          └────┘  └──────┘
typ          └────┘└┘└──────┘
doc          └────┘  └──────┘
txt          └────┘  └──────┘
par          └────┘  └──────┘
pid                └──────┘
st   ───────────────────────┘└─
419          exact (sub_eq_zero_iff_le.2 $ le_of_lt $ oadd_lt_oadd_2 h₁ h₂ $
id                  └────────────────┘     └──────┘   └────────────┘ └┘ └┘
src          └────┘ └────────────────┘└─┘ └──────┘ └────────────┘     
typ          └────┘ └────────────────┘└─┘ └──────┘ └────────────┘└┘└┘ 
doc          └────┘                   └─┘                             
txt          └────┘                   └─┘                             
par          └────┘                   └─┘                             
pid                                  └─┘                             
st   ────────────────────────────────────────────────────────────────────────
420            lt_of_le_of_ne (nat.sub_eq_zero_iff_le.1 mn) (mt pnat.eq en)).symm } },
id             └────────────┘  └────────────────────┘   └┘   └┘ └─────┘ └┘
src  ─────────┘└────────────┘ └────────────────────┘└─┘  └┘ └┘└─────┘  └──────┘
typ  ─────────┘└────────────┘ └────────────────────┘└─┘└┘└┘ └┘└─────┘└┘└──────┘
doc  ─────────┘                                     └─┘  └┘            └──────┘
txt  ─────────┘                                     └─┘  └┘            └──────┘
par  ─────────┘                                     └─┘  └┘            └──────┘
pid  ─────────┘                                     └─┘  └┘            └────┘└┘
st   ────────────────────────────────────────────────────────────────────────────┘└──┘
421      { simp [nat.succ_pnat, -nat.cast_succ],
id               └───────────┘
src        └────┘└───────────┘└───────────────┘
typ        └────┘└───────────┘└───────────────┘
doc        └────┘└───────────┘└───────────────┘
txt        └────┘             └───────────────┘
par        └────┘             └───────────────┘
pid                         └───────────────┘
st   ─────────────────────────────────────────┘└─
422        rw [(nat.sub_eq_iff_eq_add $ le_of_lt $ nat.lt_of_sub_eq_succ mn).1 mn,
id              └───────────────────┘   └──────┘   └───────────────────┘       └┘
src        └──┘ └───────────────────┘ └──────┘ └───────────────────┘  └──┘  └─
typ        └──┘ └───────────────────┘ └──────┘ └───────────────────┘  └──┘└┘└─
doc        └──┘                                                       └──┘  └─
txt        └──┘                                                       └──┘  └─
par        └──┘                                                       └──┘  └─
pid          └┘                                                       └──┘  └─
st   ───────────────────────────────────────────────────────────────────────────┘└─
423            add_comm, nat.cast_add, ordinal.mul_add, add_assoc, add_sub_add_cancel],
id             └──────┘  └──────────┘  └─────────────┘  └───────┘  └────────────────┘
src  ─────────┘└──────┘└┘└──────────┘└┘└─────────────┘└┘└───────┘└┘└────────────────┘
typ  ─────────┘└──────┘└┘└──────────┘└┘└─────────────┘└┘└───────┘└┘└────────────────┘
doc  ─────────┘        └┘            └┘               └┘         └┘                  
txt  ─────────┘        └┘            └┘               └┘         └┘                  
par  ─────────┘        └┘            └┘               └┘         └┘                  
pid  ─────────┘        └┘            └┘               └┘         └┘                  
st   ─────────────────┘└────────────┘└───────────────┘└─────────┘└──────────────────┘└──
424        refine (ordinal.sub_eq_of_add_eq $ add_absorp h₂.snd'.repr_lt $
id                 └──────────────────────┘   └────────┘ └─────────────┘
src        └─────┘ └──────────────────────┘ └────────┘└─────────────┘ 
typ        └─────┘ └──────────────────────┘ └────────┘└─────────────┘ 
doc        └─────┘                                                    
txt        └─────┘                                                    
par        └─────┘                                                    
pid                                                                  
st   ──────────────────────────────────────────────────────────────────────
425          le_trans _ (le_add_right _ _)).symm,
id           └──────┘    └──────────┘
src  ───────┘└──────┘└─┘ └──────────┘└─────────┘
typ  ───────┘└──────┘└─┘ └──────────┘└─────────┘
doc  ───────┘        └─┘             └─────────┘
txt  ───────┘        └─┘             └─────────┘
par  ───────┘        └─┘             └─────────┘
pid  ───────┘        └─┘             └────────┘
st   ──────────────────────────────────────────┘└─
426        simpa using mul_le_mul_left _ (nat_cast_le.2 $ nat.succ_pos _) } },
id                     └─────────────┘    └─────────┘     └──────────┘
src        └──────────┘└─────────────┘└─┘ └─────────┘└─┘ └──────────┘└──┘
typ        └──────────┘└─────────────┘└─┘ └─────────┘└─┘ └──────────┘└──┘
doc        └──────────┘               └─┘            └─┘             └──┘
txt        └──────────┘               └─┘            └─┘             └──┘
par        └──────────┘               └─┘            └─┘             └──┘
pid             └────┘               └─┘            └─┘             └─┘
st   ────────────────────────────────────────────────────────────────────┘└──┘
427    { exact (ordinal.sub_eq_of_add_eq $ add_absorp (h₂.below_of_lt ee).repr_lt $
id              └──────────────────────┘   └────────┘  └────────────┘ └┘
src      └────┘ └──────────────────────┘ └────────┘ └────────────┘  └────────┘ 
typ      └────┘ └──────────────────────┘ └────────┘ └────────────┘└┘└────────┘ 
doc      └────┘                                                     └────────┘ 
txt      └────┘                                                     └────────┘ 
par      └────┘                                                     └────────┘ 
pid                                                                └────────┘ 
st   ───────────────────────────────────────────────────────────────────────────────
428        omega_le_oadd _ _ _).symm }
id         └───────────┘
src  ─────┘└───────────┘└───────────┘
typ  ─────┘└───────────┘└───────────┘
doc  ─────┘             └───────────┘
txt  ─────┘             └───────────┘
par  ─────┘             └───────────┘
pid  ─────┘             └─────────┘└┘
st   ───────────────────────────────┘└─
429  end
st   ──┘
430  
431  /-- Multiplication of ordinal notations (correct only for normal input) -/
432  def mul : onote → onote → onote
id             └───┘  └───┘   └───┘
src            └───┘   └───┘   └───┘
typ            └───┘  └───┘   └───┘
doc            └───┘   └───┘   └───┘
433  | 0 _ := 0
434  | _ 0 := 0
435  | o₁@(oadd e₁ n₁ a₁) (oadd e₂ n₂ a₂) :=
id              └┘ └┘ └┘   └──┘ └┘ └┘ └┘
src                        └──┘
typ             └┘ └┘ └┘   └──┘ └┘ └┘ └┘
436    if e₂ = 0 then oadd e₁ (n₁ * n₂) a₁ else
id                   └──┘        
src                  └──┘        
typ                  └──┘        
437    oadd (e₁ + e₂) n₂ (mul o₁ a₂)
id     └──┘              └─┘
src    └──┘     
typ    └──┘              └─┘
438  
439  instance : has_mul onote := ⟨mul⟩
id              └─────┘ └───┘     └─┘
src             └─────┘ └───┘     └─┘
typ             └─────┘ └───┘     └─┘
doc                     └───┘     └─┘
440  
441  @[simp] theorem zero_mul (o : onote) : 0 * o = 0 := by cases o; refl
id                                 └───┘                       
src                                └───┘                  └────┘   └───┘
typ                                └───┘                 └────┘  └───┘
doc    └──┘                        └───┘                    └────┘   └───┘
txt                                                         └────┘   └───┘
par                                                         └────┘   └───┘
pid                                                                     
st                                                         └─────────────┘
442  @[simp] theorem mul_zero (o : onote) : o * 0 = 0 := by cases o; refl
id                                 └───┘                       
src                                └───┘                  └────┘   └────
typ                                └───┘                 └────┘  └────
doc    └──┘                        └───┘                    └────┘   └────
txt                                                         └────┘   └────
par                                                         └────┘   └────
pid                                                                     
st                                                         └──────────────
443  
src  
typ  
doc  
txt  
par  
pid  
st   
444  theorem oadd_mul (e₁ n₁ a₁ e₂ n₂ a₂) : oadd e₁ n₁ a₁ * oadd e₂ n₂ a₂ =
id                                          └──┘ └┘ └┘ └┘  └──┘ └┘ └┘ └┘ 
src                                         └──┘           └──┘          
typ                                         └──┘ └┘ └┘ └┘  └──┘ └┘ └┘ └┘ 
445    if e₂ = 0 then oadd e₁ (n₁ * n₂) a₁ else
id        └┘         └──┘ └┘  └┘  └┘  └┘
src                  └──┘        
typ       └┘         └──┘ └┘  └┘  └┘  └┘
446    oadd (e₁ + e₂) n₂ (oadd e₁ n₁ a₁ * a₂) := rfl
id     └──┘  └┘  └┘  └┘  └──┘ └┘ └┘ └┘  └┘     └─┘
src    └──┘              └──┘                  └─┘
typ    └──┘  └┘  └┘  └┘  └──┘ └┘ └┘ └┘  └┘     └─┘
447  
448  theorem oadd_mul_NF_below {e₁ n₁ a₁ b₁} (h₁ : NF_below (oadd e₁ n₁ a₁) b₁) :
id                                                 └──────┘  └──┘ └┘ └┘ └┘  └┘
src                                                └──────┘  └──┘
typ                                                └──────┘  └──┘ └┘ └┘ └┘  └┘
doc                                                └──────┘
449    ∀ {o₂ b₂}, NF_below o₂ b₂ → NF_below (oadd e₁ n₁ a₁ * o₂) (repr e₁ + b₂)
id       └┘ └┘   └──────┘ └┘ └┘   └──────┘  └──┘ └┘ └┘ └┘  └┘   └──┘ └┘  └┘
src               └──────┘         └──────┘  └──┘                └──┘    
typ      └┘ └┘   └──────┘ └┘ └┘   └──────┘  └──┘ └┘ └┘ └┘  └┘   └──┘ └┘  └┘
doc               └──────┘         └──────┘                       └──┘
450  | 0 b₂ h₂ := NF_below.zero
id                └───────────┘
src               └───────────┘
typ               └───────────┘
451  | (oadd e₂ n₂ a₂) b₂ h₂ := begin
id      └──┘
src     └──┘
typ     └──┘
st                              └─────
452    have IH := oadd_mul_NF_below h₂.snd,
id                └───────────────┘ └────┘
src    └─────────┘                 └────┘
typ    └─────────┘└───────────────┘└────┘
doc    └─────────┘                 
txt    └─────────┘                 
par    └─────────┘                 
pid    └─────┘└─┘                 
st   ────────────────────────────────────┘└─
453    by_cases e0 : e₂ = 0; simp [e0, oadd_mul],
id                   └┘           └┘  └──────┘
src    └───────┘  └─┘  └┘  └────┘  └┘└──────┘
typ    └───────┘  └─┘└┘└┘  └────┘└┘└┘└──────┘
doc    └───────┘  └─┘   └┘  └────┘  └┘        
txt    └───────┘  └─┘   └┘  └────┘  └┘        
par    └───────┘  └─┘   └┘  └────┘  └┘        
pid              └─┘           └┘        
st   ──────────────────────────────────────────┘└─
454    { apply NF_below.oadd h₁.fst h₁.snd,
id             └───────────┘ └────┘ └────┘
src      └────┘└───────────┘└────┘└────┘
typ      └────┘└───────────┘└────┘└────┘
doc      └────┘                   
txt      └────┘                   
par      └────┘                   
pid                              
st   ───┘└───────────────────────────────┘└─
455      simpa using (add_lt_add_iff_left (repr e₁)).2
id                    └─────────────────┘  └──┘ └┘
src      └──────────┘ └─────────────────┘ └──┘  └────
typ      └──────────┘ └─────────────────┘ └──┘└┘└────
doc      └──────────┘                     └──┘  └────
txt      └──────────┘                           └────
par      └──────────┘                           └────
pid           └────┘                           └────
st   ──────────────────────────────────────────────────
456        (lt_of_le_of_lt (ordinal.zero_le _) h₂.lt) },
id          └────────────┘  └─────────────┘    └───┘
src  ─────┘ └────────────┘ └─────────────┘└──┘└───┘└┘
typ  ─────┘ └────────────┘ └─────────────┘└──┘└───┘└┘
doc  ─────┘                               └──┘     └┘
txt  ─────┘                               └──┘     └┘
par  ─────┘                               └──┘     └┘
pid  ─────┘                               └──┘     
st   ────────────────────────────────────────────────┘└┘
457    { haveI := h₁.fst, haveI := h₂.fst,
id                └────┘           └────┘
src      └───────┘└────┘  └───────┘└────┘
typ      └───────┘└────┘  └───────┘└────┘
doc      └───────┘        └───────┘
txt      └───────┘        └───────┘
par      └───────┘        └───────┘
pid           └─┘             └─┘
st   ──────────────────┘└───────────────┘└─
458      apply NF_below.oadd, apply_instance,
id             └───────────┘
src      └────┘└───────────┘  └────────────┘
typ      └────┘└───────────┘  └────────────┘
doc      └────┘               └────────────┘
txt      └────┘               └────────────┘
par      └────┘               └────────────┘
pid           
st   ──────────────────────┘└──────────────┘└─
459      { rwa repr_add },
id             └──────┘
src        └──┘└──────┘
typ        └──┘└──────┘
doc        └──┘        
txt        └──┘        
par        └──┘        
pid                   
st   ─────┘└───────────┘└┘
460      { rw [repr_add, ordinal.add_lt_add_iff_left], exact h₂.lt } }
id             └──────┘  └─────────────────────────┘         └───┘
src        └──┘└──────┘└┘└─────────────────────────┘  └────┘└───┘
typ        └──┘└──────┘└┘└─────────────────────────┘  └────┘└───┘
doc        └──┘        └┘                             └────┘     
txt        └──┘        └┘                             └────┘     
par        └──┘        └┘                             └────┘     
pid          └┘        └┘                                       
st   ─────────────────┘└───────────────────────────┘└─────────────┘└───
461  end
st   ──┘
462  
463  instance mul_NF : ∀ o₁ o₂ [NF o₁] [NF o₂], NF (o₁ * o₂)
id                       └┘ └┘  └┘ └┘   └┘ └┘   └┘  └┘  └┘
src                             └┘      └┘      └┘     
typ                      └┘ └┘  └┘ └┘   └┘ └┘   └┘  └┘  └┘
doc                             └┘      └┘      └┘
464  | 0 o h₁ h₂ := by cases o; exact NF.zero
id                                   └─────┘
src                    └────┘   └────┘└─────┘
typ                    └────┘  └────┘└─────┘
doc                    └────┘   └────┘       
txt                    └────┘   └────┘       
par                    └────┘   └────┘       
pid                                        
st                    └──────────────────────┘
465  | (oadd e n a) o ⟨b₁, hb₁⟩ ⟨b₂, hb₂⟩ :=
id      └──┘               └─┘       └─┘
src     └──┘
typ     └──┘               └─┘       └─┘
466    ⟨_, oadd_mul_NF_below hb₁ hb₂⟩
id         └───────────────┘
src        └───────────────┘
typ        └───────────────┘
467  
468  @[simp] theorem repr_mul : ∀ o₁ o₂ [NF o₁] [NF o₂], repr (o₁ * o₂) = repr o₁ * repr o₂
id                                └┘ └┘  └┘ └┘   └┘ └┘   └──┘  └┘  └┘   └──┘ └┘  └──┘ └┘
src                                      └┘      └┘      └──┘           └──┘     └──┘
typ                               └┘ └┘  └┘ └┘   └┘ └┘   └──┘  └┘  └┘   └──┘ └┘  └──┘ └┘
doc    └──┘                              └┘      └┘      └──┘             └──┘      └──┘
469  | 0               o               h₁ h₂ := by cases o; exact (ordinal.zero_mul _).symm
id                                                                └──────────────┘
src                                                └────┘   └────┘ └──────────────┘└───────┘
typ                                                └────┘  └────┘ └──────────────┘└───────┘
doc                                                └────┘   └────┘                 └───────┘
txt                                                └────┘   └────┘                 └───────┘
par                                                └────┘   └────┘                 └───────┘
pid                                                                              └─────┘└┘
st                                                └────────────────────────────────────────┘
470  | (oadd e₁ n₁ a₁) 0               h₁ h₂ := (ordinal.mul_zero _).symm
id      └──┘                                     └──────────────┘   └──┘
src     └──┘                                     └──────────────┘   └──┘
typ     └──┘                                     └──────────────┘   └──┘
471  | (oadd e₁ n₁ a₁) (oadd e₂ n₂ a₂) h₁ h₂ := begin
id                      └──┘
src                     └──┘
typ                     └──┘
st                                              └─────
472    have IH : repr (mul _ _) = _ := @repr_mul _ _ h₁ h₂.snd,
id               └──┘  └─┘             └──────┘     └┘ └────┘
src    └────────┘└──┘ └─┘└────┘└────┘         └───┘  └────┘
typ    └────────┘└──┘ └─┘└────┘└────┘ └──────┘└───┘└┘└────┘
doc    └────────┘└──┘ └─┘└────┘ └────┘         └───┘  
txt    └────────┘        └────┘ └────┘         └───┘  
par    └────────┘        └────┘ └────┘         └───┘  
pid    └─────┘└─┘        └────┘ └┘└──┘         └───┘  
st   ────────────────────────────────────────────────────────┘└─
473    conv {to_lhs, simp [(*)]},
src    └────┘└────┘└┘└────┘ └─┘
typ    └────┘└────┘└┘└────┘ └─┘
txt    └────┘└────┘└┘└────┘ └─┘
par    └────┘└────┘└┘└────┘ └─┘
pid        └─────────────┘ └──┘
st   ───────┘└────┘└──────────┘└┘
474    have ao : repr a₁ + ω ^ repr e₁ * (n₁:ℕ) = ω ^ repr e₁ * (n₁:ℕ),
id                    └┘                            └──┘ └┘    └┘
src    └────────┘                  └┘   └──┘       
typ    └────────┘    └┘            └┘   └──┘└┘  └┘ 
doc    └────────┘                    └┘   └──┘       
txt    └────────┘                    └┘              
par    └────────┘                    └┘              
pid    └─────┘└─┘                    └┘              
st   ────────────────────────────────────────────────────────────────┘└─
475    { apply add_absorp h₁.snd'.repr_lt,
id             └────────┘ └─────────────┘
src      └────┘└────────┘└─────────────┘
typ      └────┘└────────┘└─────────────┘
doc      └────┘          
txt      └────┘          
par      └────┘          
pid                     
st   ───┘└──────────────────────────────┘└─
476      simpa using (mul_le_mul_iff_left $ power_pos _ omega_pos).2
id                    └─────────────────┘   └───────┘   └───────┘
src      └──────────┘ └─────────────────┘ └───────┘└─┘└───────┘└───
typ      └──────────┘ └─────────────────┘ └───────┘└─┘└───────┘└───
doc      └──────────┘                              └─┘         └───
txt      └──────────┘                              └─┘         └───
par      └──────────┘                              └─┘         └───
pid           └────┘                              └─┘         └───
st   ────────────────────────────────────────────────────────────────
477        (nat_cast_le.2 n₁.2) },
id          └─────────┘   └┘
src  ─────┘ └─────────┘└─┘  └──┘
typ  ─────┘ └─────────┘└─┘└┘└──┘
doc  ─────┘            └─┘  └──┘
txt  ─────┘            └─┘  └──┘
par  ─────┘            └─┘  └──┘
pid  ─────┘            └─┘  └─┘
st   ──────────────────────────┘└┘
478    by_cases e0 : e₂ = 0; simp [e0, mul],
id                   └┘            └┘  └─┘
src    └───────┘  └─┘   └┘  └────┘  └┘└─┘
typ    └───────┘  └─┘└┘ └┘  └────┘└┘└┘└─┘
doc    └───────┘  └─┘   └┘  └────┘  └┘└─┘
txt    └───────┘  └─┘   └┘  └────┘  └┘   
par    └───────┘  └─┘   └┘  └────┘  └┘   
pid              └─┘           └┘   
st   ─────────────────────────────────────┘└─
479    { cases nat.exists_eq_succ_of_ne_zero n₂.ne_zero with x xe,
id             └───────────────────────────┘ └────────┘
src      └────┘└───────────────────────────┘└────────┘└────────┘
typ      └────┘└───────────────────────────┘└────────┘└────────┘
doc      └────┘                                       └────────┘
txt      └────┘                                       └────────┘
par      └────┘                                       └────────┘
pid                                                  └────────┘
st   ───┘└──────────────────────────────────────────────────────┘└─
480      simp [h₂.zero_of_zero e0, xe, -nat.cast_succ],
id             └─────────────┘ └┘  └┘
src      └────┘└─────────────┘  └┘  └───────────────┘
typ      └────┘└─────────────┘└┘└┘└┘└───────────────┘
doc      └────┘                 └┘  └───────────────┘
txt      └────┘                 └┘  └───────────────┘
par      └────┘                 └┘  └───────────────┘
pid                           └┘  └───────────────┘
st   ────────────────────────────────────────────────┘└─
481      rw [← nat_cast_succ x, add_mul_succ _ ao, mul_assoc] },
id             └───────────┘   └──────────┘   └┘  └───────┘
src      └────┘└───────────┘ └┘└──────────┘└─┘  └┘└───────┘└┘
typ      └────┘└───────────┘└┘└──────────┘└─┘└┘└┘└───────┘└┘
doc      └────┘              └┘            └─┘  └┘         └┘
txt      └────┘              └┘            └─┘  └┘         └┘
par      └────┘              └┘            └─┘  └┘         └┘
pid        └──┘              └┘            └─┘  └┘         
st   ────────────────────────┘└─────────────────┘└─────────┘└┘
482    { haveI := h₁.fst, haveI := h₂.fst,
id                └────┘           └────┘
src      └───────┘└────┘  └───────┘└────┘
typ      └───────┘└────┘  └───────┘└────┘
doc      └───────┘        └───────┘
txt      └───────┘        └───────┘
par      └───────┘        └───────┘
pid           └─┘             └─┘
st   ──────────────────┘└───────────────┘└─
483      simp [IH, repr_add, power_add, ordinal.mul_add],
id             └┘  └──────┘  └───────┘  └─────────────┘
src      └────┘  └┘└──────┘└┘└───────┘└┘└─────────────┘
typ      └────┘└┘└┘└──────┘└┘└───────┘└┘└─────────────┘
doc      └────┘  └┘        └┘         └┘               
txt      └────┘  └┘        └┘         └┘               
par      └────┘  └┘        └┘         └┘               
pid            └┘        └┘         └┘               
st   ──────────────────────────────────────────────────┘└─
484      rw ← mul_assoc, congr' 2,
id            └───────┘
src      └───┘└───────┘  └──────┘
typ      └───┘└───────┘  └──────┘
doc      └───┘           └──────┘
txt      └───┘           └──────┘
par      └───┘           └──────┘
pid        └─┘                 
st   ─────────────────┘└────────┘└─
485      have := mt repr_inj.1 e0,
id               └┘ └──────┘   └┘
src      └──────┘└┘└──────┘└─┘
typ      └──────┘└┘└──────┘└─┘└┘
doc      └──────┘          └─┘
txt      └──────┘          └─┘
par      └──────┘          └─┘
pid      └───┘└─┘          └─┘
st   ───────────────────────────┘└─
486      rw [add_mul_limit ao (power_is_limit_left omega_is_limit this),
id           └───────────┘ └┘  └─────────────────┘ └────────────┘ └──┘
src      └──┘└───────────┘   └─────────────────┘└────────────┘    └──
typ      └──┘└───────────┘└┘ └─────────────────┘└────────────┘└──┘└──
doc      └──┘                                                     └──
txt      └──┘                                                     └──
par      └──┘                                                     └──
pid        └┘                                                     └──
st   ─────────────────────────────────────────────────────────────────┘└─
487          mul_assoc, mul_omega_dvd (nat_cast_pos.2 n₁.pos) (nat_lt_omega _)],
id           └───────┘  └───────────┘  └──────────┘   └────┘   └──────────┘
src  ───────┘└───────┘└┘└───────────┘ └──────────┘└─┘└────┘└┘ └──────────┘└──┘
typ  ───────┘└───────┘└┘└───────────┘ └──────────┘└─┘└────┘└┘ └──────────┘└──┘
doc  ───────┘         └┘                          └─┘      └┘             └──┘
txt  ───────┘         └┘                          └─┘      └┘             └──┘
par  ───────┘         └┘                          └─┘      └┘             └──┘
pid  ───────┘         └┘                          └─┘      └┘             └──┘
st   ────────────────┘└──────────────────────────────────────────────────────┘└──
488      simpa using power_dvd_power ω (one_le_iff_ne_zero.2 this) },
id                   └─────────────┘    └────────────────┘   └──┘
src      └──────────┘└─────────────┘  └────────────────┘└─┘    └┘
typ      └──────────┘└─────────────┘  └────────────────┘└─┘└──┘└┘
doc      └──────────┘                                   └─┘    └┘
txt      └──────────┘                                   └─┘    └┘
par      └──────────┘                                   └─┘    └┘
pid           └────┘                                   └─┘    
st   ─────────────────────────────────────────────────────────────┘└──
489  end
st   ──┘
490  
491  /-- Calculate division and remainder of `o` mod ω.
492    `split' o = (a, n)` means `o = ω * a + n`. -/
493  def split' : onote → onote × ℕ
id                └───┘  └───┘  
src               └───┘   └───┘  
typ               └───┘  └───┘  
doc               └───┘   └───┘
494  | 0            := (0, 0)
id                     
src                    
typ                    
495  | (oadd e n a) := if e = 0 then (0, n) else
id      └──┘                     
src     └──┘                        
typ     └──┘                     
496    let (a', m) := split' a in (oadd (e - 1) n a', m)
id     └─┘ └┘       └────┘      └──┘    
src                              └──┘    
typ    └─┘ └┘       └────┘      └──┘    
497  
498  /-- Calculate division and remainder of `o` mod ω.
499    `split o = (a, n)` means `o = a + n`, where `ω ∣ a`. -/
500  def split : onote → onote × ℕ
id               └───┘  └───┘  
src              └───┘   └───┘  
typ              └───┘  └───┘  
doc              └───┘   └───┘
501  | 0            := (0, 0)
id                     
src                    
typ                    
502  | (oadd e n a) := if e = 0 then (0, n) else
id      └──┘                     
src     └──┘                        
typ     └──┘                     
503    let (a', m) := split a in (oadd e n a', m)
id     └─┘ └┘       └───┘      └──┘
src                             └──┘
typ    └─┘ └┘       └───┘      └──┘
504  
505  /-- `scale x o` is the ordinal notation for `ω ^ x * o`. -/
506  def scale (x : onote) : onote → onote
id                  └───┘    └───┘  └───┘
src                 └───┘    └───┘   └───┘
typ                 └───┘    └───┘  └───┘
doc                 └───┘    └───┘   └───┘
507  | 0            := 0
508  | (oadd e n a) := oadd (x + e) n (scale a)
id      └──┘        └──┘          └───┘
src     └──┘           └──┘    
typ     └──┘        └──┘          └───┘
509  
510  /-- `mul_nat o n` is the ordinal notation for `o * n`. -/
511  def mul_nat : onote → ℕ → onote
id                 └───┘     └───┘
src                └───┘      └───┘
typ                └───┘     └───┘
doc                └───┘       └───┘
512  | 0            m := 0
513  | _            0 := 0
514  | (oadd e n a) (m+1) := oadd e (n * m.succ_pnat) a
id      └──┘            └──┘        └────────┘
src     └──┘                └──┘        └────────┘
typ     └──┘            └──┘        └────────┘
doc                                       └────────┘
515  
516  def power_aux (e a0 a : onote) : ℕ → ℕ → onote
id                           └───┘         └───┘
src                          └───┘          └───┘
typ                          └───┘         └───┘
doc                          └───┘            └───┘
517  | _     0     := 0
518  | 0     (m+1) := oadd e m.succ_pnat 0
id                  └──┘   └────────┘
src                  └──┘    └────────┘
typ                 └──┘   └────────┘
doc                           └────────┘
519  | (k+1) m     := scale (e + mul_nat a0 k) a + power_aux k m
id                 └───┘    └─────┘ └┘      └───────┘
src                  └───┘     └─────┘         
typ                └───┘    └─────┘ └┘      └───────┘
doc                   └───┘      └─────┘
520  
521  /-- `power o₁ o₂` calculates the ordinal notation for
522    the ordinal exponential `o₁ ^ o₂`. -/
523  def power (o₁ o₂ : onote) : onote :=
id                      └───┘    └───┘
src                     └───┘    └───┘
typ                     └───┘    └───┘
doc                     └───┘    └───┘
524  match split o₁ with
id         └───┘ └┘
src        └───┘
typ        └───┘ └┘
doc        └───┘
525  | (0, 0) := if o₂ = 0 then 1 else 0
id                 └┘ 
src                   
typ                └┘ 
526  | (0, 1) := 1
id     
src    
typ    
527  | (0, m+1) := let (b', k) := split' o₂ in
id              └─┘ └┘       └────┘ └┘
src                            └────┘
typ             └─┘ └┘       └────┘ └┘
doc                               └────┘
528    oadd b' (@has_pow.pow ℕ+ _ _ m.succ_pnat k) 0
id     └──┘      └─────────┘ └┘      └────────┘
src    └──┘      └─────────┘ └┘      └────────┘
typ    └──┘      └─────────┘ └┘      └────────┘
doc                          └┘      └────────┘
529  | (a@(oadd a0 _ _), m) := match split o₂ with
id        └──┘ └┘                  └───┘ └┘
src       └──┘                      └───┘
typ       └──┘ └┘                  └───┘ └┘
doc                                  └───┘
530    | (b, 0) := oadd (a0 * b) 1 0
id               └──┘     
src               └──┘     
typ              └──┘     
531    | (b, k+1) := let eb := a0*b in
id                   └┘      
src                            
typ                  └┘      
532      scale (eb + mul_nat a0 k) a + power_aux eb a0 (mul_nat a m) k m
id       └───┘  └┘  └─────┘          └───────┘ └┘     └─────┘
src      └───┘      └─────┘          └───────┘        └─────┘
typ      └───┘  └┘  └─────┘          └───────┘ └┘     └─────┘
doc      └───┘       └─────┘                            └─────┘
533    end
534  end
535  
536  instance : has_pow onote onote := ⟨power⟩
id              └─────┘ └───┘ └───┘     └───┘
src             └─────┘ └───┘ └───┘     └───┘
typ             └─────┘ └───┘ └───┘     └───┘
doc                     └───┘ └───┘     └───┘
537  
538  theorem power_def (o₁ o₂ : onote) : o₁ ^ o₂ = power._match_1 o₂ (split o₁) := rfl
id                              └───┘    └┘  └┘  └────────────┘ └┘  └───┘ └┘     └─┘
src                             └───┘            └────────────┘     └───┘        └─┘
typ                             └───┘    └┘  └┘  └────────────┘ └┘  └───┘ └┘     └─┘
doc                             └───┘                                 └───┘
539  
540  theorem split_eq_scale_split' : ∀ {o o' m} [NF o], split' o = (o', m) → split o = (scale 1 o', m)
id                                      └┘    └┘    └────┘   └┘      └───┘   └───┘   └┘  
src                                              └┘     └────┘             └───┘    └───┘
typ                                     └┘    └┘    └────┘   └┘      └───┘   └───┘   └┘  
doc                                              └┘     └────┘               └───┘      └───┘
541  | 0            o' m h p := by injection p; substs o' m; refl
id                                           
src                                └────────┘   └─────────┘  └───┘
typ                                └────────┘  └─────────┘  └───┘
doc                                └────────┘   └─────────┘  └───┘
txt                                └────────┘   └─────────┘  └───┘
par                                └────────┘   └─────────┘  └───┘
pid                                                  └───┘      
st                                └──────────────────────────────┘
542  | (oadd e n a) o' m h p := begin
id      └──┘
src     └──┘
typ     └──┘
st                              └─────
543    by_cases e0 : e = 0; simp [e0, split, split'] at p ⊢,
id                              └┘  └───┘  └────┘
src    └───────┘  └─┘ └┘  └────┘  └┘└───┘└┘└────┘└──────┘
typ    └───────┘  └─┘└┘  └────┘└┘└┘└───┘└┘└────┘└──────┘
doc    └───────┘  └─┘  └┘  └────┘  └┘└───┘└┘└────┘└──────┘
txt    └───────┘  └─┘  └┘  └────┘  └┘     └┘      └──────┘
par    └───────┘  └─┘  └┘  └────┘  └┘     └┘      └──────┘
pid              └─┘          └┘     └┘      └────┘
st   ─────────────────────────────────────────────────────┘└─
544    { rcases p with ⟨rfl, rfl⟩, exact ⟨rfl, rfl⟩ },
id                                            └─┘
src      └─────┘ └──────────────┘  └────┘    └┘└─┘└┘
typ      └─────┘└──────────────┘  └────┘    └┘└─┘└┘
doc      └─────┘ └──────────────┘  └────┘    └┘   └┘
txt      └─────┘ └──────────────┘  └────┘    └┘   └┘
par      └─────┘ └──────────────┘  └────┘    └┘   └┘
pid             └──────────────┘           └┘   
st   ───┘└──────────────────────┘└─────────────────┘└┘
545    { revert p, cases h' : split' a with a' m',
id                            └────┘ 
src      └──────┘  └────┘  └─┘└────┘ └─────────┘
typ      └──────┘  └────┘  └─┘└────┘└─────────┘
doc      └──────┘  └────┘  └─┘└────┘ └─────────┘
txt      └──────┘  └────┘  └─┘       └─────────┘
par      └──────┘  └────┘  └─┘       └─────────┘
pid            └┘         └─┘       └─────────┘
st   ───────────┘└──────────────────────────────┘└─
546      haveI := h.fst, haveI := h.snd,
id                └───┘           └───┘
src      └───────┘└───┘  └───────┘└───┘
typ      └───────┘└───┘  └───────┘└───┘
doc      └───────┘       └───────┘
txt      └───────┘       └───────┘
par      └───────┘       └───────┘
pid           └─┘            └─┘
st   ─────────────────┘└──────────────┘└─
547      simp [split_eq_scale_split' h', split, split'],
id             └───────────────────┘ └┘  └───┘  └────┘
src      └────┘                       └┘└───┘└┘└────┘
typ      └────┘└───────────────────┘└┘└┘└───┘└┘└────┘
doc      └────┘                       └┘└───┘└┘└────┘
txt      └────┘                       └┘     └┘      
par      └────┘                       └┘     └┘      
pid                                 └┘     └┘      
st   ─────────────────────────────────────────────────┘└─
548      have : 1 + (e - 1) = e,
id                          
src      └───────┘  └──┘ 
typ      └───────┘  └──┘ 
doc      └───────┘    └──┘ 
txt      └───────┘    └──┘ 
par      └───────┘    └──┘ 
pid      └───┘└──┘    └──┘ 
st   ─────────────────────────┘└─
549      { refine repr_inj.1 _, simp,
id                └──────┘
src        └─────┘└──────┘└──┘  └──┘
typ        └─────┘└──────┘└──┘  └──┘
doc        └─────┘        └──┘  └──┘
txt        └─────┘        └──┘  └──┘
par        └─────┘        └──┘  └──┘
pid                      └──┘
st   ─────┘└─────────────────┘└────┘└─
550        have := mt repr_inj.1 e0,
id                 └┘ └──────┘   └┘
src        └──────┘└┘└──────┘└─┘
typ        └──────┘└┘└──────┘└─┘└┘
doc        └──────┘          └─┘
txt        └──────┘          └─┘
par        └──────┘          └─┘
pid        └───┘└─┘          └─┘
st   ─────────────────────────────┘└─
551        exact add_sub_cancel_of_le (one_le_iff_ne_zero.2 this) },
id               └──────────────────┘  └────────────────┘   └──┘
src        └────┘└──────────────────┘ └────────────────┘└─┘    └┘
typ        └────┘└──────────────────┘ └────────────────┘└─┘└──┘└┘
doc        └────┘                                       └─┘    └┘
txt        └────┘                                       └─┘    └┘
par        └────┘                                       └─┘    └┘
pid                                                    └─┘    
st   ────────────────────────────────────────────────────────────┘└┘
552      intros, substs o' m, simp [scale, this] }
id                                  └───┘  └──┘
src      └────┘  └─────────┘  └────┘└───┘└┘    └┘
typ      └────┘  └─────────┘  └────┘└───┘└┘└──┘└┘
doc      └────┘  └─────────┘  └────┘└───┘└┘    └┘
txt      └────┘  └─────────┘  └────┘     └┘    └┘
par      └────┘  └─────────┘  └────┘     └┘    └┘
pid                    └───┘           └┘    
st   ─────────┘└───────────┘└───────────────────┘└─
553  end
st   ──┘
554  
555  theorem NF_repr_split' : ∀ {o o' m} [NF o], split' o = (o', m) → NF o' ∧ repr o = ω * repr o' + m
id                               └┘    └┘    └────┘   └┘      └┘ └┘  └──┘     └──┘ └┘  
src                                       └┘     └────┘             └┘     └──┘      └──┘    
typ                              └┘    └┘    └────┘   └┘      └┘ └┘  └──┘     └──┘ └┘  
doc                                       └┘     └────┘               └┘      └──┘        └──┘
556  | 0            o' m h p := by injection p; substs o' m; simp [NF.zero]
id                                                                └─────┘
src                                └────────┘   └─────────┘  └────┘└─────┘└┘
typ                                └────────┘  └─────────┘  └────┘└─────┘└┘
doc                                └────────┘   └─────────┘  └────┘       └┘
txt                                └────────┘   └─────────┘  └────┘       └┘
par                                └────────┘   └─────────┘  └────┘       └┘
pid                                                  └───┘             
st                                └────────────────────────────────────────┘
557  | (oadd e n a) o' m h p := begin
id      └──┘
src     └──┘
typ     └──┘
st                              └─────
558    by_cases e0 : e = 0; simp [e0, split, split'] at p ⊢,
id                              └┘  └───┘  └────┘
src    └───────┘  └─┘ └┘  └────┘  └┘└───┘└┘└────┘└──────┘
typ    └───────┘  └─┘└┘  └────┘└┘└┘└───┘└┘└────┘└──────┘
doc    └───────┘  └─┘  └┘  └────┘  └┘└───┘└┘└────┘└──────┘
txt    └───────┘  └─┘  └┘  └────┘  └┘     └┘      └──────┘
par    └───────┘  └─┘  └┘  └────┘  └┘     └┘      └──────┘
pid              └─┘          └┘     └┘      └────┘
st   ─────────────────────────────────────────────────────┘└─
559    { rcases p with ⟨rfl, rfl⟩,
id              
src      └─────┘ └──────────────┘
typ      └─────┘└──────────────┘
doc      └─────┘ └──────────────┘
txt      └─────┘ └──────────────┘
par      └─────┘ └──────────────┘
pid             └──────────────┘
st   ───┘└──────────────────────┘└─
560      simp [h.zero_of_zero e0, NF.zero] },
id             └────────────┘ └┘  └─────┘
src      └────┘└────────────┘  └┘└─────┘└┘
typ      └────┘└────────────┘└┘└┘└─────┘└┘
doc      └────┘                └┘       └┘
txt      └────┘                └┘       └┘
par      └────┘                └┘       └┘
pid                          └┘       
st   ─────────────────────────────────────┘└┘
561    { revert p, cases h' : split' a with a' m',
id                            └────┘ 
src      └──────┘  └────┘  └─┘└────┘ └─────────┘
typ      └──────┘  └────┘  └─┘└────┘└─────────┘
doc      └──────┘  └────┘  └─┘└────┘ └─────────┘
txt      └──────┘  └────┘  └─┘       └─────────┘
par      └──────┘  └────┘  └─┘       └─────────┘
pid            └┘         └─┘       └─────────┘
st   ───────────┘└──────────────────────────────┘└─
562      haveI := h.fst, haveI := h.snd,
id                └───┘           └───┘
src      └───────┘└───┘  └───────┘└───┘
typ      └───────┘└───┘  └───────┘└───┘
doc      └───────┘       └───────┘
txt      └───────┘       └───────┘
par      └───────┘       └───────┘
pid           └─┘            └─┘
st   ─────────────────┘└──────────────┘└─
563      cases NF_repr_split' h' with IH₁ IH₂,
id             └────────────┘ └┘
src      └────┘                └───────────┘
typ      └────┘└────────────┘└┘└───────────┘
doc      └────┘                └───────────┘
txt      └────┘                └───────────┘
par      └────┘                └───────────┘
pid                           └───────────┘
st   ───────────────────────────────────────┘└─
564      simp [IH₂, split'],
id             └─┘  └────┘
src      └────┘   └┘└────┘
typ      └────┘└─┘└┘└────┘
doc      └────┘   └┘└────┘
txt      └────┘   └┘      
par      └────┘   └┘      
pid             └┘      
st   ─────────────────────┘└─
565      intros, substs o' m,
src      └────┘  └─────────┘
typ      └────┘  └─────────┘
doc      └────┘  └─────────┘
txt      └────┘  └─────────┘
par      └────┘  └─────────┘
pid                    └───┘
st   ─────────┘└───────────┘└─
566      have : ω ^ repr e = ω ^ (1 : ordinal.{0}) * ω ^ (repr e - 1),
id                                   └─────┘            └──┘  
src      └─────┘          └──┘└─────┘└────┘   └──┘ └─┘
typ      └─────┘          └──┘└─────┘└────┘   └──┘└─┘
doc      └─────┘           └──┘└─────┘└────┘    └──┘  └─┘
txt      └─────┘           └──┘       └────┘          └─┘
par      └─────┘           └──┘       └────┘          └─┘
pid      └───┘└┘           └──┘       └────┘          └─┘
st   ───────────────────────────────────────────────────────────────┘└─
567      { have := mt repr_inj.1 e0,
id                 └┘ └──────┘   └┘
src        └──────┘└┘└──────┘└─┘
typ        └──────┘└┘└──────┘└─┘└┘
doc        └──────┘          └─┘
txt        └──────┘          └─┘
par        └──────┘          └─┘
pid        └───┘└─┘          └─┘
st   ─────┘└──────────────────────┘└─
568        rw [← power_add, add_sub_cancel_of_le (one_le_iff_ne_zero.2 this)] },
id               └───────┘  └──────────────────┘  └────────────────┘   └──┘
src        └────┘└───────┘└┘└──────────────────┘ └────────────────┘└─┘    └─┘
typ        └────┘└───────┘└┘└──────────────────┘ └────────────────┘└─┘└──┘└─┘
doc        └────┘         └┘                                       └─┘    └─┘
txt        └────┘         └┘                                       └─┘    └─┘
par        └────┘         └┘                                       └─┘    └─┘
pid          └──┘         └┘                                       └─┘    └┘
st   ────────────────────┘└────────────────────────────────────────────────┘└┘
569      refine ⟨NF.oadd (by apply_instance) _ _, _⟩,
id               └─────┘
src      └─────┘ └─────┘   └────────────┘└───────┘
typ      └─────┘ └─────┘   └────────────┘└───────┘
doc      └─────┘           └────────────┘└───────┘
txt      └─────┘           └────────────┘└───────┘
par      └─────┘           └────────────┘└───────┘
pid                       └──────────────────────┘
st   ──────────────────────┘└─────────────┘└───────┘└─
570      { simp at this ⊢,
src        └────────────┘
typ        └────────────┘
doc        └────────────┘
txt        └────────────┘
par        └────────────┘
pid            └───────┘
st   ─────┘└────────────┘└─
571        refine IH₁.below_of_lt' ((mul_lt_mul_iff_left omega_pos).1 $
id                └──────────────┘   └─────────────────┘ └───────┘
src        └─────┘└──────────────┘  └─────────────────┘└───────┘└──┘ 
typ        └─────┘└──────────────┘  └─────────────────┘└───────┘└──┘ 
doc        └─────┘                                              └──┘ 
txt        └─────┘                                              └──┘ 
par        └─────┘                                              └──┘ 
pid                                                            └──┘ 
st   ───────────────────────────────────────────────────────────────────
572          lt_of_le_of_lt (le_add_right _ m') _),
id           └────────────┘  └──────────┘   └┘
src  ───────┘└────────────┘ └──────────┘└─┘  └──┘
typ  ───────┘└────────────┘ └──────────┘└─┘└┘└──┘
doc  ───────┘                           └─┘  └──┘
txt  ───────┘                           └─┘  └──┘
par  ───────┘                           └─┘  └──┘
pid  ───────┘                           └─┘  └──┘
st   ────────────────────────────────────────────┘└─
573        rw [← this, ← IH₂], exact h.snd'.repr_lt },
id               └──┘    └─┘         └────────────┘
src        └────┘    └──┘     └────┘└────────────┘
typ        └────┘└──┘└──┘└─┘  └────┘└────────────┘
doc        └────┘    └──┘     └────┘              
txt        └────┘    └──┘     └────┘              
par        └────┘    └──┘     └────┘              
pid          └──┘    └──┘                        
st   ───────────────┘└─────┘└──────────────────────┘└┘
574      { rw this, simp [ordinal.mul_add, mul_assoc] } }
id            └──┘        └─────────────┘  └───────┘
src        └─┘      └────┘└─────────────┘└┘└───────┘└┘
typ        └─┘└──┘  └────┘└─────────────┘└┘└───────┘└┘
doc        └─┘      └────┘               └┘         └┘
txt        └─┘      └────┘               └┘         └┘
par        └─┘      └────┘               └┘         └┘
pid                                   └┘         
st   ────────────┘└──────────────────────────────────┘└───
575  end
st   ──┘
576  
577  theorem scale_eq_mul (x) [NF x] : ∀ o [NF o], scale x o = oadd x 1 0 * o
id                             └┘         └┘    └───┘    └──┘       
src                            └┘           └┘     └───┘      └──┘       
typ                            └┘         └┘    └───┘    └──┘       
doc                            └┘           └┘     └───┘
578  | 0            h := rfl
id                       └─┘
src                      └─┘
typ                      └─┘
579  | (oadd e n a) h := begin
id      └──┘
src     └──┘
typ     └──┘
st                       └─────
580    simp [(*)], simp [mul, scale],
id                       └─┘  └───┘
src    └────┘ └─┘  └────┘└─┘└┘└───┘
typ    └────┘ └─┘  └────┘└─┘└┘└───┘
doc    └────┘ └─┘  └────┘└─┘└┘└───┘
txt    └────┘ └─┘  └────┘   └┘     
par    └────┘ └─┘  └────┘   └┘     
pid         └─┘         └┘     
st   ───────────┘└─────────────────┘└─
581    haveI := h.snd,
id              └───┘
src    └───────┘└───┘
typ    └───────┘└───┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid         └─┘
st   ───────────────┘└─
582    by_cases e0 : e = 0,
id                    
src    └───────┘  └─┘ └┘
typ    └───────┘  └─┘└┘
doc    └───────┘  └─┘  └┘
txt    └───────┘  └─┘  └┘
par    └───────┘  └─┘  └┘
pid              └─┘  
st   ────────────────────┘└─
583    { rw scale_eq_mul, simp [e0, h.zero_of_zero, show x + 0 = x, from repr_inj.1 (by simp)] },
id          └──────────┘        └┘                                    └──────┘
src      └─┘              └────┘  └┘              └┘     └─┘  └─────┘└──────┘└─┘   └──────┘
typ      └─┘└──────────┘  └────┘└┘└┘└────────────┘└┘     └─┘└─────┘└──────┘└─┘   └──────┘
doc      └─┘              └────┘  └┘              └┘      └─┘  └─────┘        └─┘   └──────┘
txt      └─┘              └────┘  └┘              └┘      └─┘  └─────┘        └─┘   └──────┘
par      └─┘              └────┘  └┘              └┘      └─┘  └─────┘        └─┘   └──────┘
pid                            └┘              └┘      └─┘  └─────┘        └─┘   └─────┘
st   ───┘└─────────────┘└─────────────────────────────────────────────────────────────┘└───┘└─┘└┘
584    { simp [e0, scale_eq_mul, (*)] }
id             └┘  └──────────┘
src      └────┘  └┘            └┘ └──┘
typ      └────┘└┘└┘└──────────┘└┘ └──┘
doc      └────┘  └┘            └┘ └──┘
txt      └────┘  └┘            └┘ └──┘
par      └────┘  └┘            └┘ └──┘
pid            └┘            └┘ └─┘
st   ────────────────────────────────┘└─
585  end
st   ──┘
586  
587  instance NF_scale (x) [NF x] (o) [NF o] : NF (scale x o) :=
id                          └┘        └┘     └┘  └───┘  
src                         └┘         └┘      └┘  └───┘
typ                         └┘        └┘     └┘  └───┘  
doc                         └┘         └┘      └┘  └───┘
588  by rw scale_eq_mul; apply_instance
id         └──────────┘
src     └─┘└──────────┘  └──────────────
typ     └─┘└──────────┘  └──────────────
doc     └─┘              └──────────────
txt     └─┘              └──────────────
par     └─┘              └──────────────
pid                                   
st     └────────────────────────────────
589  
src  
typ  
doc  
txt  
par  
pid  
st   
590  @[simp] theorem repr_scale (x) [NF x] (o) [NF o] : repr (scale x o) = ω ^ repr x * repr o :=
id                                   └┘        └┘     └──┘  └───┘       └──┘   └──┘ 
src                                  └┘         └┘      └──┘  └───┘         └──┘    └──┘
typ                                  └┘        └┘     └──┘  └───┘       └──┘   └──┘ 
doc    └──┘                          └┘         └┘      └──┘  └───┘           └──┘     └──┘
591  by simp [scale_eq_mul]
id            └──────────┘
src     └────┘└──────────┘└─
typ     └────┘└──────────┘└─
doc     └────┘            └─
txt     └────┘            └─
par     └────┘            └─
pid                     
st     └────────────────────
592  
src  
typ  
doc  
txt  
par  
pid  
st   
593  theorem NF_repr_split {o o' m} [NF o] (h : split o = (o', m)) : NF o' ∧ repr o = repr o' + m :=
id                                   └┘        └───┘   └┘       └┘ └┘  └──┘   └──┘ └┘  
src                                  └┘         └───┘              └┘     └──┘    └──┘    
typ                                  └┘        └───┘   └┘       └┘ └┘  └──┘   └──┘ └┘  
doc                                  └┘         └───┘                └┘      └──┘     └──┘
594  begin
st   └─────
595    cases e : split' o with a n,
id               └────┘ 
src    └────┘ └─┘└────┘ └───────┘
typ    └────┘ └─┘└────┘└───────┘
doc    └────┘ └─┘└────┘ └───────┘
txt    └────┘ └─┘       └───────┘
par    └────┘ └─┘       └───────┘
pid          └─┘       └───────┘
st   ────────────────────────────┘└─
596    cases NF_repr_split' e with s₁ s₂, resetI,
id           └────────────┘ 
src    └────┘└────────────┘ └─────────┘  └────┘
typ    └────┘└────────────┘└─────────┘  └────┘
doc    └────┘               └─────────┘  └────┘
txt    └────┘               └─────────┘  └────┘
par    └────┘               └─────────┘  └────┘
pid                        └─────────┘
st   ──────────────────────────────────┘└─────────
597    rw split_eq_scale_split' e at h,
id        └───────────────────┘ 
src    └─┘└───────────────────┘ └───┘
typ    └─┘└───────────────────┘└───┘
doc    └─┘                      └───┘
txt    └─┘                      └───┘
par    └─┘                      └───┘
pid                            └───┘
st   ────────────────────────────────┘└─
598    injection h, substs o' n,
id               
src    └────────┘   └─────────┘
typ    └────────┘  └─────────┘
doc    └────────┘   └─────────┘
txt    └────────┘   └─────────┘
par    └────────┘   └─────────┘
pid                      └───┘
st   ────────────┘└───────────┘└─
599    simp [repr_scale, s₂.symm],
id           └────────┘
src    └────┘└────────┘└┘       
typ    └────┘└────────┘└┘└─────┘
doc    └────┘          └┘       
txt    └────┘          └┘       
par    └────┘          └┘       
pid                  └┘       
st   ───────────────────────────┘└─
600    apply_instance
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid                  
st   ────────────────┘
601  end
st   └─┘
602  
603  theorem split_dvd {o o' m} [NF o] (h : split o = (o', m)) : ω ∣ repr o' :=
id                               └┘        └───┘   └┘         └──┘ └┘
src                              └┘         └───┘                └──┘
typ                              └┘        └───┘   └┘         └──┘ └┘
doc                              └┘         └───┘                   └──┘
604  begin
st   └─────
605    cases e : split' o with a n,
id               └────┘ 
src    └────┘ └─┘└────┘ └───────┘
typ    └────┘ └─┘└────┘└───────┘
doc    └────┘ └─┘└────┘ └───────┘
txt    └────┘ └─┘       └───────┘
par    └────┘ └─┘       └───────┘
pid          └─┘       └───────┘
st   ────────────────────────────┘└─
606    rw split_eq_scale_split' e at h,
id        └───────────────────┘ 
src    └─┘└───────────────────┘ └───┘
typ    └─┘└───────────────────┘└───┘
doc    └─┘                      └───┘
txt    └─┘                      └───┘
par    └─┘                      └───┘
pid                            └───┘
st   ────────────────────────────────┘└─
607    injection h, subst o',
id                       └┘
src    └────────┘   └────┘
typ    └────────┘  └────┘└┘
doc    └────────┘   └────┘
txt    └────────┘   └────┘
par    └────────┘   └────┘
pid                     
st   ────────────┘└────────┘└─
608    cases NF_repr_split' e, resetI, simp [dvd_mul]
id           └────────────┘                 └─────┘
src    └────┘└────────────┘   └────┘  └────┘└─────┘└┘
typ    └────┘└────────────┘  └────┘  └────┘└─────┘└┘
doc    └────┘                 └────┘  └────┘       └┘
txt    └────┘                 └────┘  └────┘       └┘
par    └────┘                 └────┘  └────┘       └┘
pid                                             
st   ───────────────────────┘└───────────────────────┘
609  end
st   └─┘
610  
611  theorem split_add_lt {o e n a m} [NF o] (h : split o = (oadd e n a, m)) : repr a + m < ω ^ repr e :=
id                                     └┘        └───┘   └──┘          └──┘       └──┘ 
src                                    └┘         └───┘    └──┘              └──┘         └──┘
typ                                    └┘        └───┘   └──┘          └──┘       └──┘ 
doc                                    └┘         └───┘                        └──┘            └──┘
612  begin
st   └─────
613    cases NF_repr_split h with h₁ h₂,
id           └───────────┘ 
src    └────┘└───────────┘ └─────────┘
typ    └────┘└───────────┘└─────────┘
doc    └────┘              └─────────┘
txt    └────┘              └─────────┘
par    └────┘              └─────────┘
pid                       └─────────┘
st   ─────────────────────────────────┘└─
614    cases h₁.of_dvd_omega (split_dvd h) with e0 d,
id           └─────────────┘  └───────┘ 
src    └────┘└─────────────┘ └───────┘ └─────────┘
typ    └────┘└─────────────┘ └───────┘└─────────┘
doc    └────┘                          └─────────┘
txt    └────┘                          └─────────┘
par    └────┘                          └─────────┘
pid                                   └────────┘
st   ──────────────────────────────────────────────┘└─
615    have := h₁.fst, have := h₁.snd,
id             └────┘          └────┘
src    └──────┘└────┘  └──────┘└────┘
typ    └──────┘└────┘  └──────┘└────┘
doc    └──────┘        └──────┘
txt    └──────┘        └──────┘
par    └──────┘        └──────┘
pid    └───┘└─┘        └───┘└─┘
st   ───────────────┘└──────────────┘└─
616    refine add_lt_omega_power h₁.snd'.repr_lt (lt_of_lt_of_le (nat_lt_omega _) _),
id            └────────────────┘ └─────────────┘  └────────────┘  └──────────┘
src    └─────┘└────────────────┘└─────────────┘ └────────────┘ └──────────┘└────┘
typ    └─────┘└────────────────┘└─────────────┘ └────────────┘ └──────────┘└────┘
doc    └─────┘                                                             └────┘
txt    └─────┘                                                             └────┘
par    └─────┘                                                             └────┘
pid                                                                       └────┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
617    simpa using power_le_power_right omega_pos (one_le_iff_ne_zero.2 e0),
id                 └──────────────────┘ └───────┘  └────────────────┘   └┘
src    └──────────┘└──────────────────┘└───────┘ └────────────────┘└─┘  
typ    └──────────┘└──────────────────┘└───────┘ └────────────────┘└─┘└┘
doc    └──────────┘                                                └─┘  
txt    └──────────┘                                                └─┘  
par    └──────────┘                                                └─┘  
pid         └────┘                                                └─┘  
st   ─────────────────────────────────────────────────────────────────────┘└─
618  end
st   ──┘
619  
620  @[simp] theorem mul_nat_eq_mul (n o) : mul_nat o n = o * of_nat n :=
id                                          └─────┘      └────┘ 
src                                         └─────┘         └────┘
typ                                         └─────┘      └────┘ 
doc    └──┘                                 └─────┘           └────┘
621  by cases o; cases n; refl
id                    
src     └────┘   └────┘   └────
typ     └────┘  └────┘  └────
doc     └────┘   └────┘   └────
txt     └────┘   └────┘   └────
par     └────┘   └────┘   └────
pid                         
st     └───────────────────────
622  
src  
typ  
doc  
txt  
par  
pid  
st   
623  instance NF_mul_nat (o) [NF o] (n) : NF (mul_nat o n) :=
id                            └┘         └┘  └─────┘  
src                           └┘          └┘  └─────┘
typ                           └┘         └┘  └─────┘  
doc                           └┘          └┘  └─────┘
624  by simp; apply_instance
src     └──┘  └──────────────
typ     └──┘  └──────────────
doc     └──┘  └──────────────
txt     └──┘  └──────────────
par     └──┘  └──────────────
pid                         
st     └─────────────────────
625  
src  
typ  
doc  
txt  
par  
pid  
st   
626  instance NF_power_aux (e a0 a) [NF e] [NF a0] [NF a] : ∀ k m, NF (power_aux e a0 a k m)
id                                   └┘    └┘ └┘   └┘          └┘  └───────┘  └┘   
src                                  └┘     └┘      └┘             └┘  └───────┘
typ                                  └┘    └┘ └┘   └┘          └┘  └───────┘  └┘   
doc                                  └┘     └┘      └┘             └┘
627  | k     0     := by cases k; exact NF.zero
id                                     └─────┘
src                      └────┘   └────┘└─────┘
typ                      └────┘  └────┘└─────┘
doc                      └────┘   └────┘       
txt                      └────┘   └────┘       
par                      └────┘   └────┘       
pid                                          
st                      └──────────────────────┘
628  | 0     (m+1) := NF.oadd_zero _ _
id                   └──────────┘
src                  └──────────┘
typ                  └──────────┘
629  | (k+1) (m+1) := by haveI := NF_power_aux k;
id                              └──────────┘ 
src                    └───────┘            
typ                    └───────┘└──────────┘
doc                      └───────┘            
txt                      └───────┘            
par                      └───────┘            
pid                           └─┘            
st                      └─────────────────────────
630    simp [power_aux, nat.succ_ne_zero]; apply_instance
id           └───────┘  └──────────────┘
src    └────┘└───────┘└┘└──────────────┘  └──────────────
typ    └────┘└───────┘└┘└──────────────┘  └──────────────
doc    └────┘         └┘                  └──────────────
txt    └────┘         └┘                  └──────────────
par    └────┘         └┘                  └──────────────
pid                 └┘                                
st   ─────────────────────────────────────────────────────
631  
src  
typ  
doc  
txt  
par  
pid  
st   
632  instance NF_power (o₁ o₂) [NF o₁] [NF o₂] : NF (o₁ ^ o₂) :=
id                              └┘ └┘   └┘ └┘    └┘  └┘  └┘
src                             └┘      └┘       └┘     
typ                             └┘ └┘   └┘ └┘    └┘  └┘  └┘
doc                             └┘      └┘       └┘
633  begin
st   └─────
634    cases e₁ : split o₁ with a m,
id                └───┘ └┘
src    └────┘  └─┘└───┘  └───────┘
typ    └────┘  └─┘└───┘└┘└───────┘
doc    └────┘  └─┘└───┘  └───────┘
txt    └────┘  └─┘       └───────┘
par    └────┘  └─┘       └───────┘
pid           └─┘       └───────┘
st   ─────────────────────────────┘└─
635    have na := (NF_repr_split e₁).1,
id                 └───────────┘ └┘
src    └─────────┘ └───────────┘  └─┘
typ    └─────────┘ └───────────┘└┘└─┘
doc    └─────────┘                └─┘
txt    └─────────┘                └─┘
par    └─────────┘                └─┘
pid    └─────┘└─┘                └┘
st   ────────────────────────────────┘└─
636    cases e₂ : split' o₂ with b' k,
id                └────┘ └┘
src    └────┘  └─┘└────┘  └────────┘
typ    └────┘  └─┘└────┘└┘└────────┘
doc    └────┘  └─┘└────┘  └────────┘
txt    └────┘  └─┘        └────────┘
par    └────┘  └─┘        └────────┘
pid           └─┘        └────────┘
st   ───────────────────────────────┘└─
637    haveI := (NF_repr_split' e₂).1,
id               └────────────┘ └┘
src    └───────┘ └────────────┘  └─┘
typ    └───────┘ └────────────┘└┘└─┘
doc    └───────┘                 └─┘
txt    └───────┘                 └─┘
par    └───────┘                 └─┘
pid         └─┘                 └┘
st   ───────────────────────────────┘└─
638    cases a with a0 n a',
id           
src    └────┘ └───────────┘
typ    └────┘└───────────┘
doc    └────┘ └───────────┘
txt    └────┘ └───────────┘
par    └────┘ └───────────┘
pid          └───────────┘
st   ─────────────────────┘└─
639    { cases m with m,
id             
src      └────┘ └─────┘
typ      └────┘└─────┘
doc      └────┘ └─────┘
txt      └────┘ └─────┘
par      └────┘ └─────┘
pid            └─────┘
st   ───┘└────────────┘└─
640      { by_cases o₂ = 0; simp [pow, power, e₁, h]; apply_instance },
id                  └┘                 └───┘  └┘  
src        └───────┘   └┘  └────┘   └┘└───┘└┘  └┘   └─────────────┘
typ        └───────┘└┘ └┘  └────┘   └┘└───┘└┘└┘└┘  └─────────────┘
doc        └───────┘   └┘  └────┘   └┘└───┘└┘  └┘   └─────────────┘
txt        └───────┘   └┘  └────┘   └┘     └┘  └┘   └─────────────┘
par        └───────┘   └┘  └────┘   └┘     └┘  └┘   └─────────────┘
pid                            └┘     └┘  └┘                 
st   ─────┘└────────────────────────────────────────────────────────┘└┘
641      { by_cases m = 0; simp [pow, power, e₁, e₂, h]; apply_instance } },
id                                   └───┘  └┘  └┘  
src        └───────┘  └┘  └────┘   └┘└───┘└┘  └┘  └┘   └─────────────┘
typ        └───────┘ └┘  └────┘   └┘└───┘└┘└┘└┘└┘└┘  └─────────────┘
doc        └───────┘  └┘  └────┘   └┘└───┘└┘  └┘  └┘   └─────────────┘
txt        └───────┘  └┘  └────┘   └┘     └┘  └┘  └┘   └─────────────┘
par        └───────┘  └┘  └────┘   └┘     └┘  └┘  └┘   └─────────────┘
pid                           └┘     └┘  └┘  └┘                 
st   ──────────────────────────────────────────────────────────────────┘└──┘
642    { simp [pow, power, e₁, e₂, split_eq_scale_split' e₂],
id                  └───┘  └┘  └┘  └───────────────────┘ └┘
src      └────┘   └┘└───┘└┘  └┘  └┘└───────────────────┘  
typ      └────┘   └┘└───┘└┘└┘└┘└┘└┘└───────────────────┘└┘
doc      └────┘   └┘└───┘└┘  └┘  └┘                       
txt      └────┘   └┘     └┘  └┘  └┘                       
par      └────┘   └┘     └┘  └┘  └┘                       
pid             └┘     └┘  └┘  └┘                       
st   ──────────────────────────────────────────────────────┘└─
643      have := na.fst,
id               └────┘
src      └──────┘└────┘
typ      └──────┘└────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └───┘└─┘
st   ─────────────────┘└─
644      cases k with k; simp [succ_eq_add_one, power]; apply_instance }
id                            └─────────────┘  └───┘
src      └────┘ └─────┘  └────┘└─────────────┘└┘└───┘  └─────────────┘
typ      └────┘└─────┘  └────┘└─────────────┘└┘└───┘  └─────────────┘
doc      └────┘ └─────┘  └────┘               └┘└───┘  └─────────────┘
txt      └────┘ └─────┘  └────┘               └┘       └─────────────┘
par      └────┘ └─────┘  └────┘               └┘       └─────────────┘
pid            └─────┘                     └┘                     
st   ─────────────────────────────────────────────────────────────────┘└─
645  end
st   ──┘
646  
647  theorem scale_power_aux (e a0 a : onote) [NF e] [NF a0] [NF a] :
id                                     └───┘   └┘    └┘ └┘   └┘ 
src                                    └───┘   └┘     └┘      └┘
typ                                    └───┘   └┘    └┘ └┘   └┘ 
doc                                    └───┘   └┘     └┘      └┘
648    ∀ k m, repr (power_aux e a0 a k m) = ω ^ repr e * repr (power_aux 0 a0 a k m)
id          └──┘  └───────┘  └┘        └──┘   └──┘  └───────┘   └┘   
src           └──┘  └───────┘                └──┘    └──┘  └───────┘
typ         └──┘  └───────┘  └┘        └──┘   └──┘  └───────┘   └┘   
doc           └──┘                             └──┘     └──┘
649  | 0     m := by cases m; simp [power_aux]
id                                 └───────┘
src                  └────┘   └────┘└───────┘└┘
typ                  └────┘  └────┘└───────┘└┘
doc                  └────┘   └────┘         └┘
txt                  └────┘   └────┘         └┘
par                  └────┘   └────┘         └┘
pid                                       
st                  └─────────────────────────┘
650  | (k+1) m := by by_cases m = 0; simp [h, power_aux,
id                                        └───────┘
src                 └───────┘ └┘  └────┘ └┘└───────┘└─
typ                 └───────┘└┘  └────┘└┘└───────┘└─
doc                  └───────┘  └┘  └────┘ └┘         └─
txt                  └───────┘  └┘  └────┘ └┘         └─
par                  └───────┘  └┘  └────┘ └┘         └─
pid                                   └┘         └─
st                  └────────────────────────────────────
651    ordinal.mul_add, power_add, mul_assoc, scale_power_aux]
id     └─────────────┘  └───────┘  └───────┘  └─────────────┘
src  ─┘└─────────────┘└┘└───────┘└┘└───────┘└┘               └─
typ  ─┘└─────────────┘└┘└───────┘└┘└───────┘└┘└─────────────┘└─
doc  ─┘               └┘         └┘         └┘               └─
txt  ─┘               └┘         └┘         └┘               └─
par  ─┘               └┘         └┘         └┘               └─
pid  ─┘               └┘         └┘         └┘               
st   ──────────────────────────────────────────────────────────
652  
src  
typ  
doc  
txt  
par  
pid  
st   
653  theorem repr_power_aux₁ {e a} [Ne : NF e] [Na : NF a] {a' : ordinal}
id                                       └┘         └┘         └─────┘
src                                      └┘          └┘          └─────┘
typ                                      └┘         └┘         └─────┘
doc                                      └┘          └┘          └─────┘
654    (e0 : repr e ≠ 0) (h : a' < ω ^ repr e) (aa : repr a = a') (n : ℕ+) :
id           └──┘           └┘    └──┘         └──┘   └┘       └┘
src          └──┘                  └──┘          └──┘             └┘
typ          └──┘           └┘    └──┘         └──┘   └┘       └┘
doc          └──┘                     └──┘          └──┘              └┘
655    (ω ^ repr e * (n:ℕ) + a') ^ ω = (ω ^ repr e) ^ ω :=
id        └──┘        └┘        └──┘    
src       └──┘                    └──┘     
typ       └──┘        └┘        └──┘    
doc        └──┘                          └──┘      
656  begin
st   └─────
657    subst aa,
id           └┘
src    └────┘
typ    └────┘└┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────┘└─
658    have No := Ne.oadd n (Na.below_of_lt' h),
id                └─────┘   └─────────────┘ 
src    └─────────┘└─────┘  └─────────────┘ 
typ    └─────────┘└─────┘ └─────────────┘
doc    └─────────┘                         
txt    └─────────┘                         
par    └─────────┘                         
pid    └─────┘└─┘                         
st   ─────────────────────────────────────────┘└─
659    have := omega_le_oadd e n a, unfold repr at this,
id             └───────────┘   
src    └──────┘└───────────┘     └─────────────────┘
typ    └──────┘└───────────┘  └─────────────────┘
doc    └──────┘                  └─────────────────┘
txt    └──────┘                  └─────────────────┘
par    └──────┘                  └─────────────────┘
pid    └───┘└─┘                        └───┘└──────┘
st   ────────────────────────────┘└───────────────────┘└─
660    refine le_antisymm _ (power_le_power_left _ this),
id            └─────────┘    └─────────────────┘   └──┘
src    └─────┘└─────────┘└─┘ └─────────────────┘└─┘    
typ    └─────┘└─────────┘└─┘ └─────────────────┘└─┘└──┘
doc    └─────┘           └─┘                    └─┘    
txt    └─────┘           └─┘                    └─┘    
par    └─────┘           └─┘                    └─┘    
pid                     └─┘                    └─┘    
st   ──────────────────────────────────────────────────┘└─
661    apply (power_le_of_limit
id            └───────────────┘
src    └────┘ └───────────────┘
typ    └────┘ └───────────────┘
doc    └────┘                  
txt    └────┘                  
par    └────┘                  
pid                           
st   ───────────────────────────
662      (ne_of_gt $ lt_of_lt_of_le (power_pos _ omega_pos) this) omega_is_limit).2,
id        └──────┘   └────────────┘  └───────┘   └───────┘  └──┘  └────────────┘
src  ───┘ └──────┘ └────────────┘ └───────┘└─┘└───────┘└┘    └┘└────────────┘└─┘
typ  ───┘ └──────┘ └────────────┘ └───────┘└─┘└───────┘└┘└──┘└┘└────────────┘└─┘
doc  ───┘                                  └─┘         └┘    └┘              └─┘
txt  ───┘                                  └─┘         └┘    └┘              └─┘
par  ───┘                                  └─┘         └┘    └┘              └─┘
pid  ───┘                                  └─┘         └┘    └┘              └┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
663    intros b l,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid          └──┘
st   ───────────┘└─
664    have := (No.below_of_lt (lt_succ_self _)).repr_lt, unfold repr at this,
id              └────────────┘  └──────────┘
src    └──────┘ └────────────┘ └──────────┘└──────────┘  └─────────────────┘
typ    └──────┘ └────────────┘ └──────────┘└──────────┘  └─────────────────┘
doc    └──────┘                            └──────────┘  └─────────────────┘
txt    └──────┘                            └──────────┘  └─────────────────┘
par    └──────┘                            └──────────┘  └─────────────────┘
pid    └───┘└─┘                            └─────────┘        └───┘└──────┘
st   ──────────────────────────────────────────────────┘└───────────────────┘└─
665    apply le_trans (power_le_power_left b $ le_of_lt this),
id           └──────┘  └─────────────────┘    └──────┘ └──┘
src    └────┘└──────┘ └─────────────────┘  └──────┘    
typ    └────┘└──────┘ └─────────────────┘ └──────┘└──┘
doc    └────┘                                          
txt    └────┘                                          
par    └────┘                                          
pid                                                   
st   ───────────────────────────────────────────────────────┘└─
666    rw [← power_mul, ← power_mul],
id           └───────┘    └───────┘
src    └────┘└───────┘└──┘└───────┘
typ    └────┘└───────┘└──┘└───────┘
doc    └────┘         └──┘         
txt    └────┘         └──┘         
par    └────┘         └──┘         
pid      └──┘         └──┘         
st   ────────────────┘└───────────┘└──
667    apply power_le_power_right omega_pos,
id           └──────────────────┘ └───────┘
src    └────┘└──────────────────┘└───────┘
typ    └────┘└──────────────────┘└───────┘
doc    └────┘                    
txt    └────┘                    
par    └────┘                    
pid                             
st   ─────────────────────────────────────┘└─
668    cases le_or_lt ω (repr e) with h h,
id           └──────┘    └──┘ 
src    └────┘└──────┘  └──┘ └────────┘
typ    └────┘└──────┘  └──┘└────────┘
doc    └────┘          └──┘ └────────┘
txt    └────┘               └────────┘
par    └────┘               └────────┘
pid                        └───────┘
st   ───────────────────────────────────┘└─
669    { apply le_trans (mul_le_mul_left _ $ le_of_lt $ lt_succ_self _),
id             └──────┘  └─────────────┘     └──────┘   └──────────┘
src      └────┘└──────┘ └─────────────┘└─┘ └──────┘ └──────────┘└─┘
typ      └────┘└──────┘ └─────────────┘└─┘ └──────┘ └──────────┘└─┘
doc      └────┘                        └─┘                      └─┘
txt      └────┘                        └─┘                      └─┘
par      └────┘                        └─┘                      └─┘
pid                                   └─┘                      └─┘
st   ───┘└────────────────────────────────────────────────────────────┘└─
670      rw [succ, add_mul_succ _ (one_add_of_omega_le h), ← succ,
id           └──┘  └──────────┘    └─────────────────┘      └──┘
src      └──┘└──┘└┘└──────────┘└─┘ └─────────────────┘ └───┘└──┘└─
typ      └──┘└──┘└┘└──────────┘└─┘ └─────────────────┘└───┘└──┘└─
doc      └──┘└──┘└┘            └─┘                     └───┘└──┘└─
txt      └──┘    └┘            └─┘                     └───┘    └─
par      └──┘    └┘            └─┘                     └───┘    └─
pid        └┘    └┘            └─┘                     └───┘    └─
st   ───────────┘└──────────────────────────────────────┘└──────┘└─
671          succ_le, mul_lt_mul_iff_left (pos_iff_ne_zero.2 e0)],
id           └─────┘  └─────────────────┘  └─────────────┘   └┘
src  ───────┘└─────┘└┘└─────────────────┘ └─────────────┘└─┘  └┘
typ  ───────┘└─────┘└┘└─────────────────┘ └─────────────┘└─┘└┘└┘
doc  ───────┘       └┘                                   └─┘  └┘
txt  ───────┘       └┘                                   └─┘  └┘
par  ───────┘       └┘                                   └─┘  └┘
pid  ───────┘       └┘                                   └─┘  └┘
st   ──────────────┘└──────────────────────────────────────────┘└──
672      exact omega_is_limit.2 _ l },
id             └────────────┘     
src      └────┘└────────────┘└───┘ 
typ      └────┘└────────────┘└───┘
doc      └────┘              └───┘ 
txt      └────┘              └───┘ 
par      └────┘              └───┘ 
pid                         └───┘ 
st   ──────────────────────────────┘└┘
673    { refine le_trans (le_of_lt $ mul_lt_omega (omega_is_limit.2 _ h) l) _,
id              └──────┘  └──────┘   └──────────┘  └────────────┘       
src      └─────┘└──────┘ └──────┘ └──────────┘ └────────────┘└───┘ └┘ └─┘
typ      └─────┘└──────┘ └──────┘ └──────────┘ └────────────┘└───┘└┘└─┘
doc      └─────┘                                             └───┘ └┘ └─┘
txt      └─────┘                                             └───┘ └┘ └─┘
par      └─────┘                                             └───┘ └┘ └─┘
pid                                                         └───┘ └┘ └─┘
st   ───────────────────────────────────────────────────────────────────────┘└─
674      simpa using mul_le_mul_right ω (one_le_iff_ne_zero.2 e0) }
id                   └──────────────┘    └────────────────┘   └┘
src      └──────────┘└──────────────┘  └────────────────┘└─┘  └┘
typ      └──────────┘└──────────────┘  └────────────────┘└─┘└┘└┘
doc      └──────────┘                                    └─┘  └┘
txt      └──────────┘                                    └─┘  └┘
par      └──────────┘                                    └─┘  └┘
pid           └────┘                                    └─┘  
st   ────────────────────────────────────────────────────────────┘└─
675  end
st   ──┘
676  
677  section
678  local infixr ^ := @pow ordinal.{0} ordinal ordinal.has_pow
id                      └─┘ └─────┘     └─────┘ └─────────────┘
src                     └─┘ └─────┘     └─────┘ └─────────────┘
typ                     └─┘ └─────┘     └─────┘ └─────────────┘
doc                         └─────┘     └─────┘
679  
680  theorem repr_power_aux₂ {a0 a'} [N0 : NF a0] [Na' : NF a'] (m : ℕ)
id                                         └┘ └┘         └┘ └┘       
src                                        └┘            └┘          
typ                                        └┘ └┘         └┘ └┘       
doc                                        └┘            └┘
681    (d : ω ∣ repr a')
id            └──┘ └┘
src           └──┘
typ           └──┘ └┘
doc            └──┘
682    (e0 : repr a0 ≠ 0) (h : repr a' + m < ω ^ repr a0) (n : ℕ+) (k : ℕ) :
id           └──┘ └┘          └──┘ └┘      └──┘ └┘       └┘       
src          └──┘             └──┘          └──┘          └┘       
typ          └──┘ └┘          └──┘ └┘      └──┘ └┘       └┘       
doc          └──┘              └──┘            └──┘          └┘
683    let R := repr (power_aux 0 a0 (oadd a0 n a' * of_nat m) k m) in
id             └──┘  └───────┘   └┘  └──┘ └┘  └┘  └────┘    
src             └──┘  └───────┘       └──┘          └────┘
typ            └──┘  └───────┘   └┘  └──┘ └┘  └┘  └────┘    
doc             └──┘                                 └────┘
684    (k ≠ 0 → R < (ω ^ repr a0) ^ succ k) ∧
id                 └──┘ └┘   └──┘   
src                  └──┘      └──┘    
typ                └──┘ └┘   └──┘   
doc                    └──┘      └──┘
685    (ω ^ repr a0) ^ k * (ω ^ repr a0 * (n:ℕ) + repr a') + R =
id        └──┘ └┘        └──┘ └┘       └──┘ └┘    
src       └──┘            └──┘           └──┘        
typ       └──┘ └┘        └──┘ └┘       └──┘ └┘    
doc       └──┘             └──┘              └──┘
686      (ω ^ repr a0 * (n:ℕ) + repr a' + m) ^ succ k :=
id          └──┘ └┘       └──┘ └┘     └──┘ 
src         └──┘           └──┘         └──┘
typ         └──┘ └┘       └──┘ └┘     └──┘ 
doc         └──┘              └──┘          └──┘
687  begin
st   └─────
688    intro,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
689    haveI No : NF (oadd a0 n a') :=
id                └┘  └──┘ └┘  └┘
src    └─────────┘└┘ └──┘     └────
typ    └─────────┘└┘ └──┘└┘└┘└────
doc    └─────────┘└┘          └────
txt    └─────────┘            └────
par    └─────────┘            └────
pid         └─┘└─┘            └───
st   ──────────────────────────────────
690      N0.oadd n (Na'.below_of_lt' $ lt_of_le_of_lt (le_add_right _ _) h),
id       └─────┘   └──────────────┘   └────────────┘  └──────────┘      
src  ───┘└─────┘  └──────────────┘ └────────────┘ └──────────┘└────┘ 
typ  ───┘└─────┘ └──────────────┘ └────────────┘ └──────────┘└────┘
doc  ───┘                                                     └────┘ 
txt  ───┘                                                     └────┘ 
par  ───┘                                                     └────┘ 
pid  ───┘                                                     └────┘ 
st   ─────────────────────────────────────────────────────────────────────┘└─
691    induction k with k IH, {cases m; simp [power_aux, R]},
id                                          └───────┘  
src    └────────┘ └────────┘   └────┘   └────┘└───────┘└┘ 
typ    └────────┘└────────┘   └────┘  └────┘└───────┘└┘
doc    └────────┘ └────────┘   └────┘   └────┘         └┘ 
txt    └────────┘ └────────┘   └────┘   └────┘         └┘ 
par    └────────┘ └────────┘   └────┘   └────┘         └┘ 
pid              └───────┘                        └┘ 
st   ──────────────────────┘└─────────────────────────────┘└┘
692    rename R R', let R := repr (power_aux 0 a0 (oadd a0 n a' * of_nat m) k m),
id                           └──┘  └───────┘       └──┘ └┘  └┘  └────┘     
src    └─────────┘  └───────┘└──┘ └───────┘└─┘   └──┘     └────┘ └┘  
typ    └─────────┘  └───────┘└──┘ └───────┘└─┘   └──┘└┘└┘└────┘ └┘
doc    └─────────┘  └───────┘└──┘          └─┘             └────┘ └┘  
txt    └─────────┘  └───────┘              └─┘                    └┘  
par    └─────────┘  └───────┘              └─┘                    └┘  
pid          └┘└─┘  └───┘└─┘              └─┘                    └┘  
st   ────────────┘└────────────────────────────────────────────────────────────┘└─
693    let ω0 := ω ^ repr a0, let α' := ω0 * n + repr a',
id                  └──┘ └┘            └┘    └──┘ └┘
src    └────────┘ └──┘    └────────┘   └──┘
typ    └────────┘ └──┘└┘  └────────┘└┘└──┘└┘
doc    └────────┘ └──┘    └────────┘    └──┘
txt    └────────┘          └────────┘         
par    └────────┘          └────────┘         
pid    └────┘└─┘          └────┘└─┘         
st   ──────────────────────┘└──────────────────────────┘└─
694    change (k ≠ 0 → R < ω0 ^ succ k) ∧ ω0 ^ k * α' + R = (α' + m) ^ succ k at IH,
id                                      └┘               └┘       └──┘ 
src    └─────┘  └─┘          └┘               └┘ └──┘ └────┘
typ    └─────┘  └─┘          └┘ └┘       └┘ └┘ └──┘└────┘
doc    └─────┘   └─┘           └┘                └┘ └──┘ └────┘
txt    └─────┘   └─┘           └┘                └┘      └────┘
par    └─────┘   └─┘           └┘                └┘      └────┘
pid             └─┘           └┘                └┘      └───┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
695    have RR : R' = ω0 ^ k * (α' * m) + R,
id               └┘   └┘       └┘       
src    └────────┘             └┘ 
typ    └────────┘└┘ └┘   └┘ └┘ 
doc    └────────┘             └┘ 
txt    └────────┘             └┘ 
par    └────────┘             └┘ 
pid    └─────┘└─┘             └┘ 
st   ─────────────────────────────────────┘└─
696    { by_cases m = 0; simp [h, R', power_aux, R, power_mul],
id                              └┘  └───────┘    └───────┘
src      └───────┘  └┘  └────┘ └┘  └┘└───────┘└┘ └┘└───────┘
typ      └───────┘ └┘  └────┘└┘└┘└┘└───────┘└┘└┘└───────┘
doc      └───────┘  └┘  └────┘ └┘  └┘         └┘ └┘         
txt      └───────┘  └┘  └────┘ └┘  └┘         └┘ └┘         
par      └───────┘  └┘  └────┘ └┘  └┘         └┘ └┘         
pid                       └┘  └┘         └┘ └┘         
st   ───┘└───────────────────────────────────────────────────┘└─
697      { cases k; simp [power_aux] }, { refl } },
id                       └───────┘
src        └────┘   └────┘└───────┘└┘     └───┘
typ        └────┘  └────┘└───────┘└┘     └───┘
doc        └────┘   └────┘         └┘     └───┘
txt        └────┘   └────┘         └┘     └───┘
par        └────┘   └────┘         └┘     └───┘
pid                                      
st   ─────┘└────────────────────────┘└┘└──────┘└──┘
698    have α0 : 0 < α', {simpa [α', lt_def, repr] using oadd_pos a0 n a'},
id                   └┘          └┘  └────┘  └──┘        └──────┘ └┘  └┘
src    └──────────┘      └─────┘  └┘└────┘└┘└──┘└──────┘└──────┘   
typ    └──────────┘ └┘   └─────┘└┘└┘└────┘└┘└──┘└──────┘└──────┘└┘└┘
doc    └──────────┘      └─────┘  └┘      └┘└──┘└──────┘           
txt    └──────────┘      └─────┘  └┘      └┘    └──────┘           
par    └──────────┘      └─────┘  └┘      └┘    └──────┘           
pid    └─────┘└───┘             └┘      └┘    └────┘           
st   ─────────────────┘└────────────────────────────────────────────────┘└┘
699    have ω00 : 0 < ω0 ^ k := power_pos _ (power_pos _ omega_pos),
id                    └┘                    └───────┘   └───────┘
src    └───────────┘     └──┘         └─┘ └───────┘└─┘└───────┘
typ    └───────────┘ └┘ └──┘         └─┘ └───────┘└─┘└───────┘
doc    └───────────┘     └──┘         └─┘          └─┘         
txt    └───────────┘     └──┘         └─┘          └─┘         
par    └───────────┘     └──┘         └─┘          └─┘         
pid    └──────┘└───┘     └──┘         └─┘          └─┘         
st   ─────────────────────────────────────────────────────────────┘└─
700    have Rl : R < ω ^ (repr a0 * succ ↑k),
id                       └──┘ └┘   └──┘ 
src    └────────┘     └──┘   └──┘ 
typ    └────────┘    └──┘└┘ └──┘
doc    └────────┘     └──┘   └──┘  
txt    └────────┘                  
par    └────────┘                  
pid    └─────┘└─┘                  
st   ──────────────────────────────────────┘└─
701    { by_cases k0 : k = 0,
id                     
src      └───────┘  └─┘  └┘
typ      └───────┘  └─┘ └┘
doc      └───────┘  └─┘  └┘
txt      └───────┘  └─┘  └┘
par      └───────┘  └─┘  └┘
pid                └─┘  
st   ───┘└─────────────────┘└─
702      { simp [k0],
id               └┘
src        └────┘  
typ        └────┘└┘
doc        └────┘  
txt        └────┘  
par        └────┘  
pid              
st   ─────┘└───────┘└─
703        refine lt_of_lt_of_le _ (power_le_power_right omega_pos (one_le_iff_ne_zero.2 e0)),
id                └────────────┘    └──────────────────┘ └───────┘  └────────────────┘   └┘
src        └─────┘└────────────┘└─┘ └──────────────────┘└───────┘ └────────────────┘└─┘  └┘
typ        └─────┘└────────────┘└─┘ └──────────────────┘└───────┘ └────────────────┘└─┘└┘└┘
doc        └─────┘              └─┘                                                 └─┘  └┘
txt        └─────┘              └─┘                                                 └─┘  └┘
par        └─────┘              └─┘                                                 └─┘  └┘
pid                            └─┘                                                 └─┘  └┘
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
704        cases m with m; simp [k0, R, power_aux, omega_pos],
id                              └┘    └───────┘  └───────┘
src        └────┘ └─────┘  └────┘  └┘ └┘└───────┘└┘└───────┘
typ        └────┘└─────┘  └────┘└┘└┘└┘└───────┘└┘└───────┘
doc        └────┘ └─────┘  └────┘  └┘ └┘         └┘         
txt        └────┘ └─────┘  └────┘  └┘ └┘         └┘         
par        └────┘ └─────┘  └────┘  └┘ └┘         └┘         
pid              └─────┘        └┘ └┘         └┘         
st   ───────────────────────────────────────────────────────┘└─
705        rw [← nat.cast_succ], apply nat_lt_omega },
id               └───────────┘         └──────────┘
src        └────┘└───────────┘  └────┘└──────────┘
typ        └────┘└───────────┘  └────┘└──────────┘
doc        └────┘               └────┘            
txt        └────┘               └────┘            
par        └────┘               └────┘            
pid          └──┘                                
st   ────────────────────────┘└───────────────────┘└┘
706      { rw power_mul, exact IH.1 k0 } },
id            └───────┘        └┘   └┘
src        └─┘└───────┘  └────┘  └─┘  
typ        └─┘└───────┘  └────┘└┘└─┘└┘
doc        └─┘           └────┘  └─┘  
txt        └─┘           └────┘  └─┘  
par        └─┘           └────┘  └─┘  
pid                            └─┘  
st   ─────────────────┘└──────────────┘└──┘
707    refine ⟨λ_, _, _⟩,
src    └─────┘  └──────┘
typ    └─────┘  └──────┘
doc    └─────┘  └──────┘
txt    └─────┘  └──────┘
par    └─────┘  └──────┘
pid            └──────┘
st   ──────────────────┘└─
708    { rw [RR, ← power_mul _ _ (succ k.succ)],
id           └┘    └───────┘      └──┘ └────┘
src      └──┘  └──┘└───────┘└───┘ └──┘└────┘└┘
typ      └──┘└┘└──┘└───────┘└───┘ └──┘└────┘└┘
doc      └──┘  └──┘         └───┘ └──┘      └┘
txt      └──┘  └──┘         └───┘           └┘
par      └──┘  └──┘         └───┘           └┘
pid        └┘  └──┘         └───┘           └┘
st   ───┘└────┘└─────────────────────────────┘└──
709      have e0 := pos_iff_ne_zero.2 e0,
id                  └─────────────┘   └┘
src      └─────────┘└─────────────┘└─┘
typ      └─────────┘└─────────────┘└─┘└┘
doc      └─────────┘               └─┘
txt      └─────────┘               └─┘
par      └─────────┘               └─┘
pid      └─────┘└─┘               └─┘
st   ──────────────────────────────────┘└─
710      have rr0 := lt_of_lt_of_le e0 (le_add_left _ _),
id                   └────────────┘ └┘  └─────────┘
src      └──────────┘└────────────┘   └─────────┘└───┘
typ      └──────────┘└────────────┘└┘ └─────────┘└───┘
doc      └──────────┘                            └───┘
txt      └──────────┘                            └───┘
par      └──────────┘                            └───┘
pid      └──────┘└─┘                            └───┘
st   ──────────────────────────────────────────────────┘└─
711      apply add_lt_omega_power,
id             └────────────────┘
src      └────┘└────────────────┘
typ      └────┘└────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────────────┘└─
712      { simp [power_mul, ω0, power_add],
id               └───────┘  └┘  └───────┘
src        └────┘└───────┘└┘  └┘└───────┘
typ        └────┘└───────┘└┘└┘└┘└───────┘
doc        └────┘         └┘  └┘         
txt        └────┘         └┘  └┘         
par        └────┘         └┘  └┘         
pid                     └┘  └┘         
st   ─────┘└─────────────────────────────┘└─
713        rw [mul_lt_mul_iff_left ω00, ← ordinal.power_add],
id             └─────────────────┘ └─┘    └───────────────┘
src        └──┘└─────────────────┘   └──┘└───────────────┘
typ        └──┘└─────────────────┘└─┘└──┘└───────────────┘
doc        └──┘                      └──┘                 
txt        └──┘                      └──┘                 
par        └──┘                      └──┘                 
pid          └┘                      └──┘                 
st   ────────────────────────────────┘└───────────────────┘└──
714        have := (No.below_of_lt _).repr_lt, unfold repr at this,
id                  └────────────┘
src        └──────┘ └────────────┘└─────────┘  └─────────────────┘
typ        └──────┘ └────────────┘└─────────┘  └─────────────────┘
doc        └──────┘               └─────────┘  └─────────────────┘
txt        └──────┘               └─────────┘  └─────────────────┘
par        └──────┘               └─────────┘  └─────────────────┘
pid        └───┘└─┘               └────────┘        └───┘└──────┘
st   ───────────────────────────────────────┘└───────────────────┘└─
715        refine mul_lt_omega_power rr0 this (nat_lt_omega _),
id                └────────────────┘ └─┘ └──┘  └──────────┘
src        └─────┘└────────────────┘        └──────────┘└─┘
typ        └─────┘└────────────────┘└─┘└──┘ └──────────┘└─┘
doc        └─────┘                                      └─┘
txt        └─────┘                                      └─┘
par        └─────┘                                      └─┘
pid                                                    └─┘
st   ────────────────────────────────────────────────────────┘└─
716        simpa using (add_lt_add_iff_left (repr a0)).2 e0 },
id                      └─────────────────┘  └──┘ └┘     └┘
src        └──────────┘ └─────────────────┘ └──┘  └───┘  
typ        └──────────┘ └─────────────────┘ └──┘└┘└───┘└┘
doc        └──────────┘                     └──┘  └───┘  
txt        └──────────┘                           └───┘  
par        └──────────┘                           └───┘  
pid             └────┘                           └───┘  
st   ──────────────────────────────────────────────────────┘└┘
717      { refine lt_of_lt_of_le Rl (power_le_power_right omega_pos $
id                └────────────┘ └┘  └──────────────────┘ └───────┘
src        └─────┘└────────────┘   └──────────────────┘└───────┘ 
typ        └─────┘└────────────┘└┘ └──────────────────┘└───────┘ 
doc        └─────┘                                               
txt        └─────┘                                               
par        └─────┘                                               
pid                                                             
st   ─────────────────────────────────────────────────────────────────
718          mul_le_mul_left _ $ succ_le_succ.2 $ nat_cast_le.2 $ le_of_lt k.lt_succ_self) } },
id           └─────────────┘     └──────────┘     └─────────┘     └──────┘ └────────────┘
src  ───────┘└─────────────┘└─┘ └──────────┘└─┘ └─────────┘└─┘ └──────┘└────────────┘└┘
typ  ───────┘└─────────────┘└─┘ └──────────┘└─┘ └─────────┘└─┘ └──────┘└────────────┘└┘
doc  ───────┘               └─┘             └─┘            └─┘                       └┘
txt  ───────┘               └─┘             └─┘            └─┘                       └┘
par  ───────┘               └─┘             └─┘            └─┘                       └┘
pid  ───────┘               └─┘             └─┘            └─┘                       
st   ─────────────────────────────────────────────────────────────────────────────────────┘└──┘
719    refine calc
src    └─────┘    
typ    └─────┘    
doc    └─────┘    
txt    └─────┘    
par    └─────┘    
pid              
st   ──────────────
720          ω0 ^ k.succ * α' + R'
id                              └┘
src  ───────┘               
typ  ───────┘             └┘
doc  ───────┘               
txt  ───────┘               
par  ───────┘               
pid  ───────┘               
st   ──────────────────────────────
721        = ω0 ^ succ k * α' + (ω0 ^ k * α' * m + R) : by rw [nat_cast_succ, RR, ← mul_assoc]
id                └──┘           └┘      └┘                 └───────────┘  └┘    └───────┘
src  ─────┘    └──┘                 └──┘  └──┘└───────────┘└┘  └──┘└───────┘└─
typ  ─────┘    └──┘      └┘  └┘  └──┘  └──┘└───────────┘└┘└┘└──┘└───────┘└─
doc  ─────┘    └──┘                 └──┘  └──┘             └┘  └──┘         └─
txt  ─────┘                         └──┘  └──┘             └┘  └──┘         └─
par  ─────┘                         └──┘  └──┘             └┘  └──┘         └─
pid  ─────┘                         └──┘  └───┘             └┘  └──┘         └─
st   ────────────────────────────────────────────────────┘└────────────────┘└──┘└───────────┘
722    ... = (ω0 ^ k * α' + R) * α' + (ω0 ^ k * α' + R) * m : _
src  ─┘└──┘           └┘              └┘  └────
typ  ─┘└──┘           └┘              └┘  └────
doc  ─┘└──┘           └┘              └┘  └────
txt  ─┘└──┘           └┘              └┘  └────
par  ─┘└──┘           └┘              └┘  └────
pid  ─────┘           └┘              └┘  └────
st   ─┘└────────────────────────────────────────────────────────
723    ... = (α' + m) ^ succ k.succ : by rw [← ordinal.mul_add, ← nat_cast_succ, power_succ, IH.2],
id                           └────┘            └─────────────┘    └───────────┘  └────────┘  └┘
src  ─────┘      └┘     └────┘└─┘  └────┘└─────────────┘└──┘└───────────┘└┘└────────┘└┘  └─┘
typ  ─────┘      └┘     └────┘└─┘  └────┘└─────────────┘└──┘└───────────┘└┘└────────┘└┘└┘└─┘
doc  ─────┘      └┘           └─┘  └────┘               └──┘             └┘          └┘  └─┘
txt  ─────┘      └┘           └─┘  └────┘               └──┘             └┘          └┘  └─┘
par  ─────┘      └┘           └─┘  └────┘               └──┘             └┘          └┘  └─┘
pid  ─────┘      └┘           └─┘  └─────┘               └──┘             └┘          └┘  └─┘
st   ──────────────────────────────────┘└────────────────────┘└───────────────┘└──────────┘└──┘└─┘└─
724    congr' 1,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          
st   ─────────┘└─
725    { have αd : ω ∣ α' := dvd_add (dvd_mul_of_dvd _
id                    └┘    └─────┘  └────────────┘
src      └────────┘   └──┘└─────┘ └────────────┘└──
typ      └────────┘ └┘└──┘└─────┘ └────────────┘└──
doc      └────────┘    └──┘                      └──
txt      └────────┘    └──┘                      └──
par      └────────┘    └──┘                      └──
pid      └─────┘└─┘    └──┘                      └──
st   ───┘└─────────────────────────────────────────────
726        (by simpa using power_dvd_power ω (one_le_iff_ne_zero.2 e0))) d,
id                         └─────────────┘    └────────────────┘   └┘    
src  ─────┘   └──────────┘└─────────────┘  └────────────────┘└─┘  └─┘
typ  ─────┘   └──────────┘└─────────────┘  └────────────────┘└─┘└┘└─┘
doc  ─────┘   └──────────┘                                   └─┘  └─┘
txt  ─────┘   └──────────┘                                   └─┘  └─┘
par  ─────┘   └──────────┘                                   └─┘  └─┘
pid  ─────┘   └───────────┘                                   └─┘  └──┘
st   ────────┘└──────────────────────────────────────────────────────┘└──┘└─
727      rw [ordinal.mul_add (ω0 ^ k), add_assoc, ← mul_assoc, ← power_succ,
id           └─────────────┘  └┘      └───────┘    └───────┘    └────────┘
src      └──┘└─────────────┘     └─┘└───────┘└──┘└───────┘└──┘└────────┘└─
typ      └──┘└─────────────┘ └┘ └─┘└───────┘└──┘└───────┘└──┘└────────┘└─
doc      └──┘                    └─┘         └──┘         └──┘          └─
txt      └──┘                    └─┘         └──┘         └──┘          └─
par      └──┘                    └─┘         └──┘         └──┘          └─
pid        └┘                    └─┘         └──┘         └──┘          └─
st   ───────────────────────────────┘└─────────┘└───────────┘└────────────┘└─
728          add_mul_limit _ (is_limit_iff_omega_dvd.2 ⟨ne_of_gt α0, αd⟩), mul_assoc,
id           └───────────┘    └────────────────────┘    └──────┘ └┘  └┘    └───────┘
src  ───────┘└───────────┘└─┘ └────────────────────┘└─┘ └──────┘  └┘  └──┘└───────┘└─
typ  ───────┘└───────────┘└─┘ └────────────────────┘└─┘ └──────┘└┘└┘└┘└──┘└───────┘└─
doc  ───────┘             └─┘                       └─┘           └┘  └──┘         └─
txt  ───────┘             └─┘                       └─┘           └┘  └──┘         └─
par  ───────┘             └─┘                       └─┘           └┘  └──┘         └─
pid  ───────┘             └─┘                       └─┘           └┘  └──┘         └─
st   ───────────────────────────────────────────────────────────────────┘└─────────┘└─
729          @mul_omega_dvd n (nat_cast_pos.2 n.pos) (nat_lt_omega _) _ αd],
id            └───────────┘    └──────────┘   └───┘   └──────────┘      └┘
src  ───────┘ └───────────┘  └──────────┘└─┘└───┘└┘ └──────────┘└────┘  
typ  ───────┘ └───────────┘  └──────────┘└─┘└───┘└┘ └──────────┘└────┘└┘
doc  ───────┘                            └─┘     └┘             └────┘  
txt  ───────┘                            └─┘     └┘             └────┘  
par  ───────┘                            └─┘     └┘             └────┘  
pid  ───────┘                            └─┘     └┘             └────┘  
st   ────────────────────────────────────────────────────────────────────┘└──
730      apply @add_absorp _ (repr a0 * succ k),
id              └────────┘    └──┘ └┘   └──┘ 
src      └────┘ └────────┘└─┘ └──┘   └──┘ 
typ      └────┘ └────────┘└─┘ └──┘└┘ └──┘
doc      └────┘           └─┘ └──┘   └──┘ 
txt      └────┘           └─┘             
par      └────┘           └─┘             
pid                      └─┘             
st   ─────────────────────────────────────────┘└─
731      { refine add_lt_omega_power _ Rl,
id                └────────────────┘   └┘
src        └─────┘└────────────────┘└─┘
typ        └─────┘└────────────────┘└─┘└┘
doc        └─────┘                  └─┘
txt        └─────┘                  └─┘
par        └─────┘                  └─┘
pid                                └─┘
st   ─────┘└────────────────────────────┘└─
732        rw [power_mul, power_succ, mul_lt_mul_iff_left ω00],
id             └───────┘  └────────┘  └─────────────────┘ └─┘
src        └──┘└───────┘└┘└────────┘└┘└─────────────────┘   
typ        └──┘└───────┘└┘└────────┘└┘└─────────────────┘└─┘
doc        └──┘         └┘          └┘                      
txt        └──┘         └┘          └┘                      
par        └──┘         └┘          └┘                      
pid          └┘         └┘          └┘                      
st   ──────────────────┘└──────────┘└───────────────────────┘└──
733        exact No.snd'.repr_lt },
id               └─────────────┘
src        └────┘└─────────────┘
typ        └────┘└─────────────┘
doc        └────┘               
txt        └────┘               
par        └────┘               
pid                            
st   ───────────────────────────┘└┘
734      { have := mul_le_mul_left (ω0 ^ succ k) (one_le_iff_pos.2 $ nat_cast_pos.2 n.pos),
id                 └─────────────┘  └┘   └──┘    └────────────┘     └──────────┘   └───┘
src        └──────┘└─────────────┘    └──┘ └┘ └────────────┘└─┘ └──────────┘└─┘└───┘
typ        └──────┘└─────────────┘ └┘ └──┘└┘ └────────────┘└─┘ └──────────┘└─┘└───┘
doc        └──────┘                   └──┘ └┘               └─┘             └─┘     
txt        └──────┘                        └┘               └─┘             └─┘     
par        └──────┘                        └┘               └─┘             └─┘     
pid        └───┘└─┘                        └┘               └─┘             └─┘     
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
735        rw power_mul, simpa [-power_succ] } },
id            └───────┘
src        └─┘└───────┘  └──────────────────┘
typ        └─┘└───────┘  └──────────────────┘
doc        └─┘           └──────────────────┘
txt        └─┘           └──────────────────┘
par        └─┘           └──────────────────┘
pid                          └───────────┘
st   ─────────────────┘└────────────────────┘└──┘
736    { cases m,
id             
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────┘└─
737      { have : R = 0, {cases k; simp [R, power_aux]}, simp [this] },
id                                       └───────┘          └──┘
src        └─────┘  └┘   └────┘   └────┘ └┘└───────┘   └────┘    └┘
typ        └─────┘ └┘   └────┘  └────┘└┘└───────┘   └────┘└──┘└┘
doc        └─────┘  └┘   └────┘   └────┘ └┘            └────┘    └┘
txt        └─────┘  └┘   └────┘   └────┘ └┘            └────┘    └┘
par        └─────┘  └┘   └────┘   └────┘ └┘            └────┘    └┘
pid        └───┘└┘                  └┘                    
st   ─────┘└──────────┘└─────────────────────────────┘└┘└───────────┘└┘
738      { rw [← nat_cast_succ, add_mul_succ],
id               └───────────┘  └──────────┘
src        └────┘└───────────┘└┘└──────────┘
typ        └────┘└───────────┘└┘└──────────┘
doc        └────┘             └┘            
txt        └────┘             └┘            
par        └────┘             └┘            
pid          └──┘             └┘            
st   ────────────────────────┘└────────────┘└─
739        apply add_absorp Rl,
id               └────────┘ └┘
src        └────┘└────────┘
typ        └────┘└────────┘└┘
doc        └────┘          
txt        └────┘          
par        └────┘          
pid                       
st   ────────────────────────┘└─
740        rw [power_mul, power_succ],
id             └───────┘  └────────┘
src        └──┘└───────┘└┘└────────┘
typ        └──┘└───────┘└┘└────────┘
doc        └──┘         └┘          
txt        └──┘         └┘          
par        └──┘         └┘          
pid          └┘         └┘          
st   ──────────────────┘└──────────┘└──
741        apply ordinal.mul_le_mul_left,
id               └─────────────────────┘
src        └────┘└─────────────────────┘
typ        └────┘└─────────────────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ──────────────────────────────────┘└─
742        simpa [α', repr] using omega_le_oadd a0 n a' } }
id                └┘  └──┘        └───────────┘ └┘  └┘
src        └─────┘  └┘└──┘└──────┘└───────────┘     
typ        └─────┘└┘└┘└──┘└──────┘└───────────┘└┘└┘
doc        └─────┘  └┘└──┘└──────┘                  
txt        └─────┘  └┘    └──────┘                  
par        └─────┘  └┘    └──────┘                  
pid               └┘    └────┘                  
st   ──────────────────────────────────────────────────┘└───
743  end
st   ──┘
744  
745  end
746  
747  theorem repr_power (o₁ o₂) [NF o₁] [NF o₂] : repr (o₁ ^ o₂) = repr o₁ ^ repr o₂ :=
id                               └┘ └┘   └┘ └┘    └──┘  └┘  └┘   └──┘ └┘  └──┘ └┘
src                              └┘      └┘       └──┘           └──┘     └──┘
typ                              └┘ └┘   └┘ └┘    └──┘  └┘  └┘   └──┘ └┘  └──┘ └┘
doc                              └┘      └┘       └──┘             └──┘      └──┘
748  begin
st   └─────
749    cases e₁ : split o₁ with a m,
id                └───┘ └┘
src    └────┘  └─┘└───┘  └───────┘
typ    └────┘  └─┘└───┘└┘└───────┘
doc    └────┘  └─┘└───┘  └───────┘
txt    └────┘  └─┘       └───────┘
par    └────┘  └─┘       └───────┘
pid           └─┘       └───────┘
st   ─────────────────────────────┘└─
750    cases NF_repr_split e₁ with N₁ r₁,
id           └───────────┘ └┘
src    └────┘└───────────┘  └─────────┘
typ    └────┘└───────────┘└┘└─────────┘
doc    └────┘               └─────────┘
txt    └────┘               └─────────┘
par    └────┘               └─────────┘
pid                        └─────────┘
st   ──────────────────────────────────┘└─
751    cases a with a0 n a',
id           
src    └────┘ └───────────┘
typ    └────┘└───────────┘
doc    └────┘ └───────────┘
txt    └────┘ └───────────┘
par    └────┘ └───────────┘
pid          └───────────┘
st   ─────────────────────┘└─
752    { cases m with m,
id             
src      └────┘ └─────┘
typ      └────┘└─────┘
doc      └────┘ └─────┘
txt      └────┘ └─────┘
par      └────┘ └─────┘
pid            └─────┘
st   ───┘└────────────┘└─
753      { by_cases o₂ = 0; simp [power_def, power, e₁, h, r₁],
id                  └┘            └───────┘  └───┘  └┘    └┘
src        └───────┘   └┘  └────┘└───────┘└┘└───┘└┘  └┘ └┘  
typ        └───────┘└┘ └┘  └────┘└───────┘└┘└───┘└┘└┘└┘└┘└┘
doc        └───────┘   └┘  └────┘         └┘└───┘└┘  └┘ └┘  
txt        └───────┘   └┘  └────┘         └┘     └┘  └┘ └┘  
par        └───────┘   └┘  └────┘         └┘     └┘  └┘ └┘  
pid                                  └┘     └┘  └┘ └┘  
st   ─────┘└─────────────────────────────────────────────────┘└─
754        have := mt repr_inj.1 h, rw zero_power this },
id                 └┘ └──────┘        └────────┘ └──┘
src        └──────┘└┘└──────┘└─┘   └─┘└────────┘    
typ        └──────┘└┘└──────┘└─┘  └─┘└────────┘└──┘
doc        └──────┘          └─┘   └─┘              
txt        └──────┘          └─┘   └─┘              
par        └──────┘          └─┘   └─┘              
pid        └───┘└─┘          └─┘                   
st   ────────────────────────────┘└───────────────────┘└┘
755      { cases e₂ : split' o₂ with b' k,
id                    └────┘ └┘
src        └────┘  └─┘└────┘  └────────┘
typ        └────┘  └─┘└────┘└┘└────────┘
doc        └────┘  └─┘└────┘  └────────┘
txt        └────┘  └─┘        └────────┘
par        └────┘  └─┘        └────────┘
pid               └─┘        └────────┘
st   ───────────────────────────────────┘└─
756        cases NF_repr_split' e₂ with _ r₂,
id               └────────────┘ └┘
src        └────┘└────────────┘  └────────┘
typ        └────┘└────────────┘└┘└────────┘
doc        └────┘                └────────┘
txt        └────┘                └────────┘
par        └────┘                └────────┘
pid                             └────────┘
st   ──────────────────────────────────────┘└─
757        by_cases m = 0; simp [power_def, power, e₁, h, r₁, e₂, r₂, -nat.cast_succ],
id                              └───────┘  └───┘  └┘    └┘  └┘  └┘
src        └───────┘  └┘  └────┘└───────┘└┘└───┘└┘  └┘ └┘  └┘  └┘  └───────────────┘
typ        └───────┘ └┘  └────┘└───────┘└┘└───┘└┘└┘└┘└┘└┘└┘└┘└┘└┘└───────────────┘
doc        └───────┘  └┘  └────┘         └┘└───┘└┘  └┘ └┘  └┘  └┘  └───────────────┘
txt        └───────┘  └┘  └────┘         └┘     └┘  └┘ └┘  └┘  └┘  └───────────────┘
par        └───────┘  └┘  └────┘         └┘     └┘  └┘ └┘  └┘  └┘  └───────────────┘
pid                                 └┘     └┘  └┘ └┘  └┘  └┘  └───────────────┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
758        rw [power_add, power_mul, power_omega _ (nat_lt_omega _)],
id             └───────┘  └───────┘  └─────────┘    └──────────┘
src        └──┘└───────┘└┘└───────┘└┘└─────────┘└─┘ └──────────┘└──┘
typ        └──┘└───────┘└┘└───────┘└┘└─────────┘└─┘ └──────────┘└──┘
doc        └──┘         └┘         └┘           └─┘             └──┘
txt        └──┘         └┘         └┘           └─┘             └──┘
par        └──┘         └┘         └┘           └─┘             └──┘
pid          └┘         └┘         └┘           └─┘             └──┘
st   ──────────────────┘└─────────┘└──────────────────────────────┘└──
759        simpa using nat_cast_lt.2 (nat.succ_lt_succ $ nat.pos_iff_ne_zero.2 h) } },
id                     └─────────┘    └──────────────┘   └─────────────────┘   
src        └──────────┘└─────────┘└─┘ └──────────────┘ └─────────────────┘└─┘ └┘
typ        └──────────┘└─────────┘└─┘ └──────────────┘ └─────────────────┘└─┘└┘
doc        └──────────┘           └─┘                                     └─┘ └┘
txt        └──────────┘           └─┘                                     └─┘ └┘
par        └──────────┘           └─┘                                     └─┘ └┘
pid             └────┘           └─┘                                     └─┘ 
st   ────────────────────────────────────────────────────────────────────────────┘└──┘
760    { haveI := N₁.fst, haveI := N₁.snd,
id                └────┘           └────┘
src      └───────┘└────┘  └───────┘└────┘
typ      └───────┘└────┘  └───────┘└────┘
doc      └───────┘        └───────┘
txt      └───────┘        └───────┘
par      └───────┘        └───────┘
pid           └─┘             └─┘
st   ──────────────────┘└───────────────┘└─
761      cases N₁.of_dvd_omega (split_dvd e₁) with a00 ad,
id             └─────────────┘  └───────┘ └┘
src      └────┘└─────────────┘ └───────┘  └───────────┘
typ      └────┘└─────────────┘ └───────┘└┘└───────────┘
doc      └────┘                           └───────────┘
txt      └────┘                           └───────────┘
par      └────┘                           └───────────┘
pid                                      └──────────┘
st   ───────────────────────────────────────────────────┘└─
762      have al := split_add_lt e₁,
id                  └──────────┘ └┘
src      └─────────┘└──────────┘
typ      └─────────┘└──────────┘└┘
doc      └─────────┘            
txt      └─────────┘            
par      └─────────┘            
pid      └─────┘└─┘            
st   ─────────────────────────────┘└─
763      have aa : repr (a' + of_nat m) = repr a' + m, {simp},
id                           └────┘      └──┘ └┘   
src      └────────┘       └────┘ └┘ └──┘       └──┘
typ      └────────┘       └────┘ └┘ └──┘└┘    └──┘
doc      └────────┘        └────┘ └┘ └──┘       └──┘
txt      └────────┘               └┘            └──┘
par      └────────┘               └┘            └──┘
pid      └─────┘└─┘               └┘        
st   ───────────────────────────────────────────────┘└─────┘└┘
764      cases e₂ : split' o₂ with b' k,
id                  └────┘ └┘
src      └────┘  └─┘└────┘  └────────┘
typ      └────┘  └─┘└────┘└┘└────────┘
doc      └────┘  └─┘└────┘  └────────┘
txt      └────┘  └─┘        └────────┘
par      └────┘  └─┘        └────────┘
pid             └─┘        └────────┘
st   ─────────────────────────────────┘└─
765      cases NF_repr_split' e₂ with _ r₂,
id             └────────────┘ └┘
src      └────┘└────────────┘  └────────┘
typ      └────┘└────────────┘└┘└────────┘
doc      └────┘                └────────┘
txt      └────┘                └────────┘
par      └────┘                └────────┘
pid                           └────────┘
st   ────────────────────────────────────┘└─
766      simp [power_def, power, e₁, r₁, split_eq_scale_split' e₂],
id             └───────┘  └───┘  └┘  └┘  └───────────────────┘ └┘
src      └────┘└───────┘└┘└───┘└┘  └┘  └┘└───────────────────┘  
typ      └────┘└───────┘└┘└───┘└┘└┘└┘└┘└┘└───────────────────┘└┘
doc      └────┘         └┘└───┘└┘  └┘  └┘                       
txt      └────┘         └┘     └┘  └┘  └┘                       
par      └────┘         └┘     └┘  └┘  └┘                       
pid                   └┘     └┘  └┘  └┘                       
st   ────────────────────────────────────────────────────────────┘└─
767      cases k with k,
id             
src      └────┘ └─────┘
typ      └────┘└─────┘
doc      └────┘ └─────┘
txt      └────┘ └─────┘
par      └────┘ └─────┘
pid            └─────┘
st   ─────────────────┘└─
768      { simp [power, r₂, power_mul, repr_power_aux₁ a00 al aa] },
id               └───┘  └┘  └───────┘  └─────────────┘ └─┘ └┘ └┘
src        └────┘└───┘└┘  └┘└───────┘└┘└─────────────┘       └┘
typ        └────┘└───┘└┘└┘└┘└───────┘└┘└─────────────┘└─┘└┘└┘└┘
doc        └────┘└───┘└┘  └┘         └┘                      └┘
txt        └────┘     └┘  └┘         └┘                      └┘
par        └────┘     └┘  └┘         └┘                      └┘
pid                 └┘  └┘         └┘                      
st   ─────┘└─────────────────────────────────────────────────────┘└┘
769      { simp [succ_eq_add_one, power, r₂, power_add, power_mul, mul_assoc],
id               └─────────────┘  └───┘  └┘  └───────┘  └───────┘  └───────┘
src        └────┘└─────────────┘└┘└───┘└┘  └┘└───────┘└┘└───────┘└┘└───────┘
typ        └────┘└─────────────┘└┘└───┘└┘└┘└┘└───────┘└┘└───────┘└┘└───────┘
doc        └────┘               └┘└───┘└┘  └┘         └┘         └┘         
txt        └────┘               └┘     └┘  └┘         └┘         └┘         
par        └────┘               └┘     └┘  └┘         └┘         └┘         
pid                           └┘     └┘  └┘         └┘         └┘         
st   ───────────────────────────────────────────────────────────────────────┘└─
770        rw [repr_power_aux₁ a00 al aa, scale_power_aux], simp [power_mul],
id             └─────────────┘ └─┘ └┘ └┘  └─────────────┘         └───────┘
src        └──┘└─────────────┘       └┘└─────────────┘  └────┘└───────┘
typ        └──┘└─────────────┘└─┘└┘└┘└┘└─────────────┘  └────┘└───────┘
doc        └──┘                      └┘                 └────┘         
txt        └──┘                      └┘                 └────┘         
par        └──┘                      └┘                 └────┘         
pid          └┘                      └┘                              
st   ──────────────────────────────────┘└───────────────┘└────────────────┘└─
771        rw [← ordinal.mul_add, ← add_assoc (ω ^ repr a0 * (n:ℕ))], congr' 1,
id               └─────────────┘    └───────┘     └──┘ └┘   
src        └────┘└─────────────┘└──┘└───────┘  └──┘     └─┘  └──────┘
typ        └────┘└─────────────┘└──┘└───────┘  └──┘└┘  └─┘  └──────┘
doc        └────┘               └──┘            └──┘      └─┘  └──────┘
txt        └────┘               └──┘                      └─┘  └──────┘
par        └────┘               └──┘                      └─┘  └──────┘
pid          └──┘               └──┘                      └─┘        
st   ──────────────────────────┘└─────────────────────────────────┘└────────┘└─
772        rw [← power_succ],
id               └────────┘
src        └────┘└────────┘
typ        └────┘└────────┘
doc        └────┘          
txt        └────┘          
par        └────┘          
pid          └──┘          
st   ─────────────────────┘└──
773        exact (repr_power_aux₂ _ ad a00 al _ _).2 } }
id                └─────────────┘   └┘ └─┘ └┘
src        └────┘ └─────────────┘└─┘       └──────┘
typ        └────┘ └─────────────┘└─┘└┘└─┘└┘└──────┘
doc        └────┘                └─┘       └──────┘
txt        └────┘                └─┘       └──────┘
par        └────┘                └─┘       └──────┘
pid                             └─┘       └───┘└─┘
st   ───────────────────────────────────────────────┘└───
774  end
st   ──┘
775  
776  end onote
777  
778  /-- The type of normal ordinal notations. (It would have been
779    nicer to define this right in the inductive type, but `NF o`
780    requires `repr` which requires `onote`, so all these things
781    would have to be defined at once, which messes up the VM
782    representation.) -/
783  def nonote := {o : onote // o.NF}
id                     └───┘    └─┘
src                    └───┘     └─┘
typ                    └───┘    └─┘
doc                     └───┘     └─┘
784  
785  instance : decidable_eq nonote := by unfold nonote; apply_instance
id              └──────────┘ └────┘
src             └──────────┘ └────┘       └───────────┘  └──────────────
typ             └──────────┘ └────┘       └───────────┘  └──────────────
doc                          └────┘       └───────────┘  └──────────────
txt                                       └───────────┘  └──────────────
par                                       └───────────┘  └──────────────
pid                                             └─────┘                
st                                       └──────────────────────────────
786  
src  
typ  
doc  
txt  
par  
pid  
st   
787  namespace nonote
788  open onote
789  
790  instance NF (o : nonote) : NF o.1 := o.2
id                    └────┘    └┘      
src                   └────┘    └┘        
typ                   └────┘    └┘      
doc                   └────┘    └┘
791  
792  /-- Construct a `nonote` from an ordinal notation
793    (and infer normality) -/
794  def mk (o : onote) [h : NF o] : nonote := ⟨o, h⟩
id               └───┘       └┘     └────┘       
src              └───┘       └┘      └────┘
typ              └───┘       └┘     └────┘       
doc              └───┘       └┘      └────┘
795  
796  /-- The ordinal represented by an ordinal notation.
797    (This function is noncomputable because ordinal
798    arithmetic is noncomputable. In computational applications
799    `nonote` can be used exclusively without reference
800    to `ordinal`, but this function allows for correctness
801    results to be stated.) -/
802  noncomputable def repr (o : nonote) : ordinal := o.1.repr
id                               └────┘    └─────┘     └──┘
src                              └────┘    └─────┘      └──┘
typ                              └────┘    └─────┘     └──┘
doc                              └────┘    └─────┘       └──┘
803  
804  instance : has_to_string nonote := ⟨λ x, x.1.to_string⟩
id              └───────────┘ └────┘          └───────┘
src             └───────────┘ └────┘            └───────┘
typ             └───────────┘ └────┘          └───────┘
doc                           └────┘             └───────┘
805  instance : has_repr nonote := ⟨λ x, x.1.repr'⟩
id              └──────┘ └────┘          └───┘
src             └──────┘ └────┘            └───┘
typ             └──────┘ └────┘          └───┘
doc                      └────┘             └───┘
806  
807  instance : preorder nonote :=
id              └──────┘ └────┘
src             └──────┘ └────┘
typ             └──────┘ └────┘
doc                      └────┘
808  { le       := λ x y, repr x ≤ repr y,
id                      └──┘   └──┘ 
src                       └──┘    └──┘
typ                     └──┘   └──┘ 
doc                       └──┘     └──┘
809    lt       := λ x y, repr x < repr y,
id                      └──┘   └──┘ 
src                       └──┘    └──┘
typ                     └──┘   └──┘ 
doc                       └──┘     └──┘
810    le_refl  := λ a, @le_refl ordinal _ _,
id                      └─────┘ └─────┘
src                      └─────┘ └─────┘
typ                     └─────┘ └─────┘
doc                              └─────┘
811    le_trans := λ a b c, @le_trans ordinal _ _ _ _,
id                        └──────┘ └─────┘
src                          └──────┘ └─────┘
typ                       └──────┘ └─────┘
doc                                   └─────┘
812    lt_iff_le_not_le := λ a b, @lt_iff_le_not_le ordinal _ _ _ }
id                               └──────────────┘ └─────┘
src                                └──────────────┘ └─────┘
typ                              └──────────────┘ └─────┘
doc                                                 └─────┘
813  
814  instance : has_zero nonote := ⟨⟨0, NF.zero⟩⟩
id              └──────┘ └────┘         └─────┘
src             └──────┘ └────┘         └─────┘
typ             └──────┘ └────┘         └─────┘
doc                      └────┘
815  instance : inhabited nonote := ⟨0⟩
id              └───────┘ └────┘
src             └───────┘ └────┘
typ             └───────┘ └────┘
doc                       └────┘
816  
817  /-- Convert a natural number to an ordinal notation -/
818  def of_nat (n : ℕ) : nonote := ⟨of_nat n, _, NF_below_of_nat _⟩
id                       └────┘     └────┘      └─────────────┘
src                      └────┘     └────┘       └─────────────┘
typ                      └────┘     └────┘      └─────────────┘
doc                       └────┘     └────┘
819  
820  /-- Compare ordinal notations -/
821  def cmp (a b : nonote) : ordering :=
id                  └────┘    └──────┘
src                 └────┘    └──────┘
typ                 └────┘    └──────┘
doc                 └────┘
822  cmp a.1 b.1
id   └─┘   
src  └─┘     
typ  └─┘   
doc  └─┘
823  
824  theorem cmp_compares : ∀ a b : nonote, (cmp a b).compares a b
id                                 └────┘   └─┘   └──────┘   
src                                └────┘   └─┘     └──────┘
typ                                └────┘   └─┘   └──────┘   
doc                                 └────┘   └─┘     └──────┘
825  | ⟨a, ha⟩ ⟨b, hb⟩ := begin
st                        └─────
826    resetI,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ──────────
827    dsimp [cmp], have := onote.cmp_compares a b,
id            └─┘           └────────────────┘  
src    └─────┘└─┘  └──────┘└────────────────┘ 
typ    └─────┘└─┘  └──────┘└────────────────┘
doc    └─────┘└─┘  └──────┘                   
txt    └─────┘     └──────┘                   
par    └─────┘     └──────┘                   
pid              └───┘└─┘                   
st   ────────────┘└──────────────────────────────┘└─
828    cases onote.cmp a b; try {exact this},
id           └───────┘               └──┘
src    └────┘└───────┘    └───┘└────┘    
typ    └────┘└───────┘  └───┘└────┘└──┘
doc    └────┘└───────┘    └───┘└────┘    
txt    └────┘             └───┘└────┘    
par    └────┘             └───┘└────┘    
pid                         └──────┘    
st   ───────────────────────────┘└────────┘└┘
829    exact subtype.mk_eq_mk.2 this
id           └──────────────┘   └──┘
src    └────┘└──────────────┘└─┘    
typ    └────┘└──────────────┘└─┘└──┘
doc    └────┘                └─┘    
txt    └────┘                └─┘    
par    └────┘                └─┘    
pid                         └─┘    
st   ───────────────────────────────┘
830  end
st   └─┘
831  
832  instance : linear_order nonote :=
id              └──────────┘ └────┘
src             └──────────┘ └────┘
typ             └──────────┘ └────┘
doc                          └────┘
833  { le_antisymm := λ a b, match cmp a b, cmp_compares a b with
id                               └─┘    └──────────┘  
src                                └─┘      └──────────┘
typ                              └─┘    └──────────┘  
doc                                └─┘
834      | ordering.lt, h, h₁, h₂ := (not_lt_of_le h₂).elim h
id         └─────────┘        └┘     └──────────┘    └──┘
src        └─────────┘                └──────────┘    └──┘
typ        └─────────┘        └┘     └──────────┘    └──┘
835      | ordering.eq, h, h₁, h₂ := h
id         └─────────┘  
src        └─────────┘
typ        └─────────┘  
836      | ordering.gt, h, h₁, h₂ := (not_lt_of_le h₁).elim h
id         └─────────┘    └┘         └──────────┘    └──┘
src        └─────────┘                └──────────┘    └──┘
typ        └─────────┘    └┘         └──────────┘    └──┘
837      end,
838    le_total := λ a b, match cmp a b, cmp_compares a b with
id                            └─┘    └──────────┘  
src                             └─┘      └──────────┘
typ                           └─┘    └──────────┘  
doc                             └─┘
839      | ordering.lt, h := or.inl (le_of_lt h)
id         └─────────┘      └────┘  └──────┘
src        └─────────┘       └────┘  └──────┘
typ        └─────────┘      └────┘  └──────┘
840      | ordering.eq, h := or.inl (le_of_eq h)
id         └─────────┘      └────┘  └──────┘
src        └─────────┘       └────┘  └──────┘
typ        └─────────┘      └────┘  └──────┘
841      | ordering.gt, h := or.inr (le_of_lt h)
id         └─────────┘      └────┘  └──────┘
src        └─────────┘       └────┘  └──────┘
typ        └─────────┘      └────┘  └──────┘
842      end,
843    ..nonote.preorder }
id       └─────────────┘
src      └─────────────┘
typ      └─────────────┘
844  
845  instance decidable_lt : @decidable_rel nonote (<)
id                            └───────────┘ └────┘ 
src                           └───────────┘ └────┘ 
typ                           └───────────┘ └────┘ 
doc                                         └────┘
846  | a b := decidable_of_iff _ (cmp_compares a b).eq_lt
id          └──────────────┘    └──────────┘     └───┘
src           └──────────────┘    └──────────┘     └───┘
typ         └──────────────┘    └──────────┘     └───┘
847  
848  instance : decidable_linear_order nonote :=
id              └────────────────────┘ └────┘
src             └────────────────────┘ └────┘
typ             └────────────────────┘ └────┘
doc                                    └────┘
849  { decidable_le := λ a b, decidable_of_iff _ not_lt,
id                          └──────────────┘   └────┘
src                           └──────────────┘   └────┘
typ                         └──────────────┘   └────┘
850    decidable_lt := nonote.decidable_lt,
id                     └─────────────────┘
src                    └─────────────────┘
typ                    └─────────────────┘
851    ..nonote.linear_order }
id       └─────────────────┘
src      └─────────────────┘
typ      └─────────────────┘
852  
853  /-- Asserts that `repr a < ω ^ repr b`. Used in `nonote.rec_on` -/
854  def below (a b : nonote) : Prop := NF_below a.1 (repr b)
id                    └────┘            └──────┘    └──┘ 
src                   └────┘            └──────┘     └──┘
typ                   └────┘            └──────┘    └──┘ 
doc                   └────┘            └──────┘      └──┘
855  
856  /-- The `oadd` pseudo-constructor for `nonote` -/
857  def oadd (e : nonote) (n : ℕ+) (a : nonote) (h : below a e) : nonote := ⟨_, NF.oadd e.2 n h⟩
id                 └────┘       └┘       └────┘       └───┘      └────┘        └─────┘    
src                └────┘       └┘       └────┘       └───┘        └────┘        └─────┘  
typ                └────┘       └┘       └────┘       └───┘      └────┘        └─────┘    
doc                └────┘       └┘       └────┘       └───┘        └────┘
858  
859  /-- This is a recursor-like theorem for `nonote` suggesting an
860    inductive definition, which can't actually be defined this
861    way due to conflicting dependencies. -/
862  @[elab_as_eliminator] def rec_on {C : nonote → Sort*} (o : nonote)
id                                         └────┘               └────┘
src                                        └────┘               └────┘
typ                                        └────┘               └────┘
doc    └────────────────┘                  └────┘               └────┘
863    (H0 : C 0)
id           
typ          
864    (H1 : ∀ e n a h, C e → C a → C (oadd e n a h)) : C o :=
id                            └──┘          
src                                    └──┘
typ                           └──┘          
doc                                    └──┘
865  begin
st   └─────
866    cases o with o h, induction o with e n a IHe IHa,
id                                
src    └────┘ └───────┘  └────────┘ └─────────────────┘
typ    └────┘└───────┘  └────────┘└─────────────────┘
doc    └────┘ └───────┘  └────────┘ └─────────────────┘
txt    └────┘ └───────┘  └────────┘ └─────────────────┘
par    └────┘ └───────┘  └────────┘ └─────────────────┘
pid          └───────┘            └────────────────┘
st   ─────────────────┘└──────────────────────────────┘└─
867    { exact H0 },
id             └┘
src      └────┘  
typ      └────┘└┘
doc      └────┘  
txt      └────┘  
par      └────┘  
pid             
st   ───┘└───────┘└┘
868    { exact H1 ⟨e, h.fst⟩ n ⟨a, h.snd⟩ h.snd' (IHe _) (IHa _) }
id             └┘    └───┘      └───┘  └────┘  └─┘     └─┘
src      └────┘    └┘└───┘└┘   └┘└───┘└┘└────┘    └──┘    └──┘
typ      └────┘└┘ └┘└───┘└┘ └┘└───┘└┘└────┘ └─┘└──┘ └─┘└──┘
doc      └────┘    └┘     └┘   └┘     └┘          └──┘    └──┘
txt      └────┘    └┘     └┘   └┘     └┘          └──┘    └──┘
par      └────┘    └┘     └┘   └┘     └┘          └──┘    └──┘
pid               └┘     └┘   └┘     └┘          └──┘    └─┘
st   ───────────────────────────────────────────────────────────┘└─
869  end
st   ──┘
870  
871  /-- Addition of ordinal notations -/
872  instance : has_add nonote := ⟨λ x y, mk (x.1 + y.1)⟩
id              └─────┘ └────┘          └┘     
src             └─────┘ └────┘            └┘       
typ             └─────┘ └────┘          └┘     
doc                     └────┘            └┘
873  
874  theorem repr_add (a b) : repr (a + b) = repr a + repr b :=
id                            └──┘       └──┘   └──┘ 
src                           └──┘         └──┘    └──┘
typ                           └──┘       └──┘   └──┘ 
doc                           └──┘           └──┘     └──┘
875  onote.repr_add a.1 b.1
id   └────────────┘   
src  └────────────┘     
typ  └────────────┘   
876  
877  /-- Subtraction of ordinal notations -/
878  instance : has_sub nonote := ⟨λ x y, mk (x.1 - y.1)⟩
id              └─────┘ └────┘          └┘     
src             └─────┘ └────┘            └┘       
typ             └─────┘ └────┘          └┘     
doc                     └────┘            └┘
879  
880  theorem repr_sub (a b) : repr (a - b) = repr a - repr b :=
id                            └──┘       └──┘   └──┘ 
src                           └──┘         └──┘    └──┘
typ                           └──┘       └──┘   └──┘ 
doc                           └──┘           └──┘     └──┘
881  onote.repr_sub a.1 b.1
id   └────────────┘   
src  └────────────┘     
typ  └────────────┘   
882  
883  /-- Multiplication of ordinal notations -/
884  instance : has_mul nonote := ⟨λ x y, mk (x.1 * y.1)⟩
id              └─────┘ └────┘          └┘     
src             └─────┘ └────┘            └┘       
typ             └─────┘ └────┘          └┘     
doc                     └────┘            └┘
885  
886  theorem repr_mul (a b) : repr (a * b) = repr a * repr b :=
id                            └──┘       └──┘   └──┘ 
src                           └──┘         └──┘    └──┘
typ                           └──┘       └──┘   └──┘ 
doc                           └──┘           └──┘     └──┘
887  onote.repr_mul a.1 b.1
id   └────────────┘   
src  └────────────┘     
typ  └────────────┘   
888  
889  /-- Exponentiation of ordinal notations -/
890  def power (x y : nonote) := mk (x.1.power y.1)
id                    └────┘     └┘   └───┘  
src                   └────┘     └┘    └───┘   
typ                   └────┘     └┘   └───┘  
doc                   └────┘     └┘     └───┘
891  
892  theorem repr_power (a b) : repr (power a b) = (repr a).power (repr b) :=
id                              └──┘  └───┘      └──┘  └───┘   └──┘ 
src                             └──┘  └───┘        └──┘   └───┘   └──┘
typ                             └──┘  └───┘      └──┘  └───┘   └──┘ 
doc                             └──┘  └───┘         └──┘   └───┘   └──┘
893  onote.repr_power a.1 b.1
id   └──────────────┘   
src  └──────────────┘     
typ  └──────────────┘   
894  
895  end nonote